---

Step * of Lemma minimal-not-not-implies

∀[P,A:ℙ].  (((((P ⇒ A) ⇒ A) ⇒ (P ∨ A)) ⇒ A) ⇒ A)
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (InstLemma `minimal-not-not-xmiddle` [⌜P⌝]⋅ THENA Auto)
   THEN (D -1 With ⌜A⌝  THENA Auto)) }

1
1. [P] : ℙ
2. [A] : ℙ
3. ((P ∨ (P ⇒ A)) ⇒ A) ⇒ A
⊢ ((((P ⇒ A) ⇒ A) ⇒ (P ∨ A)) ⇒ A) ⇒ A

---

Latex:

---

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


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (InstLemma  `minimal-not-not-xmiddle`  [\mkleeneopen{}P\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}A\mkleeneclose{}    THENA  Auto))

---

Home Index