---

Step * of Lemma classical-implies

∀[A,B:ℙ].  uiff(A ⇒ {B};{A ⇒ B})
BY
{ Auto }

1
1. A : ℙ
2. B : ℙ
3. A ⇒ {B}
⊢ {A ⇒ B}

2
1. A : ℙ
2. B : ℙ
3. {A ⇒ B}
4. A@i
⊢ {B}

---

Latex:

---

Latex:
\mforall{}[A,B:\mBbbP{}].    uiff(A  {}\mRightarrow{}  \{B\};\{A  {}\mRightarrow{}  B\})


By

---

Latex:
Auto

---

Home Index