---

Step * of Lemma no-uniform-Peirce's-law

¬(∀[P,B:ℙ].  (((P ⇒ B) ⇒ P) ⇒ P))
BY
{ ((D 0 THENA Auto) THEN InstLemma `Peirce\'s-law-iff-xmiddle` [] THEN ThinTrivial THEN Thin 1) }

1
1. ∀[P,B:ℙ].  (P ∨ (P ⇒ B))
⊢ False

---

Latex:

---

Latex:
\mneg{}(\mforall{}[P,B:\mBbbP{}].    (((P  {}\mRightarrow{}  B)  {}\mRightarrow{}  P)  {}\mRightarrow{}  P))


By

---

Latex:
((D  0  THENA  Auto)  THEN  InstLemma  `Peirce\mbackslash{}'s-law-iff-xmiddle`  []  THEN  ThinTrivial  THEN  Thin  1)

---

Home Index