---

Step * 1 of Lemma implies-quotient-true2


1. [P] : ℙ
2. [Q] : ℙ
3. P ⇒ ⇃(Q)
4. ⇃(P)
5. ⇃(⇃(Q))
⊢ ⇃(Q)
BY
{ (RenameVar `x' (-1) THEN UseWitness ⌜x⌝⋅) }

1
1. P : ℙ
2. Q : ℙ
3. P ⇒ ⇃(Q)
4. ⇃(P)
5. x : ⇃(⇃(Q))
⊢ x ∈ ⇃(Q)

---

Latex:

---

Latex:

1.  [P]  :  \mBbbP{}
2.  [Q]  :  \mBbbP{}
3.  P  {}\mRightarrow{}  \00D9(Q)
4.  \00D9(P)
5.  \00D9(\00D9(Q))
\mvdash{}  \00D9(Q)


By

---

Latex:
(RenameVar  `x'  (-1)  THEN  UseWitness  \mkleeneopen{}x\mkleeneclose{}\mcdot{})

---

Home Index