---

Step * of Lemma dneg_elim_a

∀[A:ℙ]. (Dec(A) ⇒ (¬¬A ⇐⇒ A))
BY
{ Auto }

1
1. [A] : ℙ
2. Dec(A)
3. ¬¬A
⊢ A

---

Latex:

---

Latex:
\mforall{}[A:\mBbbP{}].  (Dec(A)  {}\mRightarrow{}  (\mneg{}\mneg{}A  \mLeftarrow{}{}\mRightarrow{}  A))


By

---

Latex:
Auto

---

Home Index