---

Step * of Lemma cand_functionality_wrt_iff

∀[a1,a2,b1,b2:ℙ].  ((a1 ⇐⇒ a2) ⇒ (b1 ⇐⇒ b2) ⇒ (a1 c∧ b1 ⇐⇒ a2 c∧ b2))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[a1,a2,b1,b2:\mBbbP{}].    ((a1  \mLeftarrow{}{}\mRightarrow{}  a2)  {}\mRightarrow{}  (b1  \mLeftarrow{}{}\mRightarrow{}  b2)  {}\mRightarrow{}  (a1  c\mwedge{}  b1  \mLeftarrow{}{}\mRightarrow{}  a2  c\mwedge{}  b2))


By

---

Latex:
Auto

---

Home Index