---

Step * of Lemma implies-quotient-true2

∀[P,Q:ℙ].  ((P ⇒ ⇃(Q)) ⇒ {⇃(P) ⇒ ⇃(Q)})
BY
{ (Unfold `guard` 0
   THEN RepeatFor 3 ((D 0 THENA Auto))
   THEN (InstLemma `implies-quotient-true` [⌜P⌝;⌜⇃(Q)⌝]⋅ THENA Auto)
   THEN ParallelLast) }

1
1. [P] : ℙ
2. [Q] : ℙ
3. P ⇒ ⇃(Q)
4. ⇃(P)
5. ⇃(⇃(Q))
⊢ ⇃(Q)

---

Latex:

---

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


By

---

Latex:
(Unfold  `guard`  0
  THEN  RepeatFor  3  ((D  0  THENA  Auto))
  THEN  (InstLemma  `implies-quotient-true`  [\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}\00D9(Q)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelLast)

---

Home Index