---

Step * of Lemma double-negation-iff-xmiddle

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

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

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index