---

Step * 1 of Lemma dneg_elim_a


1. [A] : ℙ
2. Dec(A)
3. ¬¬A
⊢ A
BY
{ (BLemma `dneg_elim` THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  \mBbbP{}
2.  Dec(A)
3.  \mneg{}\mneg{}A
\mvdash{}  A


By

---

Latex:
(BLemma  `dneg\_elim`  THEN  Auto)

---

Home Index