---

Step * 1 of Lemma Peirce-subtype-dneg-elim


1. x : ∀[P,B:ℙ].  (((P ⇒ B) ⇒ P) ⇒ P)
2. P : ℙ
⊢ x ∈ ∀[B:ℙ]. (((P ⇒ B) ⇒ P) ⇒ P)
BY
{ Auto }

---

Latex:

---

Latex:

1.  x  :  \mforall{}[P,B:\mBbbP{}].    (((P  {}\mRightarrow{}  B)  {}\mRightarrow{}  P)  {}\mRightarrow{}  P)
2.  P  :  \mBbbP{}
\mvdash{}  x  \mmember{}  \mforall{}[B:\mBbbP{}].  (((P  {}\mRightarrow{}  B)  {}\mRightarrow{}  P)  {}\mRightarrow{}  P)


By

---

Latex:
Auto

---

Home Index