---

Step * of Lemma not-quotient-true

∀[P:ℙ]. (¬⇃(P) ⇐⇒ ¬P)
BY
{ TACTIC:(Auto THEN Try ((ParallelLast THEN BLemma `trivial-quotient-true` THEN Auto)) THEN (D 0 THENA Auto)) }

1
1. P : ℙ
2. ¬P
3. ⇃(P)
⊢ False

---

Latex:

---

Latex:
\mforall{}[P:\mBbbP{}].  (\mneg{}\00D9(P)  \mLeftarrow{}{}\mRightarrow{}  \mneg{}P)


By

---

Latex:
TACTIC:(Auto
                THEN  Try  ((ParallelLast  THEN  BLemma  `trivial-quotient-true`  THEN  Auto))
                THEN  (D  0  THENA  Auto))

---

Home Index