---

Step * of Lemma iff_functionality_wrt_iff

∀[P1,P2,Q1,Q2:ℙ].  ((P1 ⇐⇒ P2) ⇒ (Q1 ⇐⇒ Q2) ⇒ (P1 ⇐⇒ Q1 ⇐⇒ P2 ⇐⇒ Q2))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[P1,P2,Q1,Q2:\mBbbP{}].    ((P1  \mLeftarrow{}{}\mRightarrow{}  P2)  {}\mRightarrow{}  (Q1  \mLeftarrow{}{}\mRightarrow{}  Q2)  {}\mRightarrow{}  (P1  \mLeftarrow{}{}\mRightarrow{}  Q1  \mLeftarrow{}{}\mRightarrow{}  P2  \mLeftarrow{}{}\mRightarrow{}  Q2))


By

---

Latex:
Auto

---

Home Index