---

Step * of Lemma Peirce's-law-iff-xmiddle

∀[P,B:ℙ].  (((P ⇒ B) ⇒ P) ⇒ P) ⇐⇒ ∀[P,B:ℙ].  (P ∨ (P ⇒ B))
BY
{ Auto }

1
1. ∀[P,B:ℙ].  (((P ⇒ B) ⇒ P) ⇒ P)@i'
2. [P] : ℙ
3. [B] : ℙ
⊢ P ∨ (P ⇒ B)

2
1. ∀[P,B:ℙ].  (P ∨ (P ⇒ B))@i'
2. [P] : ℙ
3. [B] : ℙ
4. (P ⇒ B) ⇒ P@i
⊢ P

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index