---

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


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

---

Latex:

---

Latex:

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


By

---

Latex:
Auto

---

Home Index