---

Step * of Lemma classical-or

∀[A,B:ℙ].  uiff(((¬A) ⇒ {B}) ∧ ((¬B) ⇒ {A});{A ∨ B})
BY
{ Auto }

1
1. A : ℙ
2. B : ℙ
3. (¬A) ⇒ {B}
4. (¬B) ⇒ {A}
⊢ {A ∨ B}

2
1. A : ℙ
2. B : ℙ
3. {A ∨ B}
4. ¬A@i
⊢ {B}

3
1. A : ℙ
2. B : ℙ
3. {A ∨ B}
4. ¬B@i
⊢ {A}

---

Latex:

---

Latex:
\mforall{}[A,B:\mBbbP{}].    uiff(((\mneg{}A)  {}\mRightarrow{}  \{B\})  \mwedge{}  ((\mneg{}B)  {}\mRightarrow{}  \{A\});\{A  \mvee{}  B\})


By

---

Latex:
Auto

---

Home Index