Theorem pm5.74i

Distribution of implication over biconditional (inference form). (Contributed by NM, 1-Aug-1994.)

Hypothesis
pm5.74i.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow \psi \leftrightarrow \varphi \rightarrow \chi \)
Proof
l0
pm5.74i.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
pm5.74
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \leftrightarrow (\varphi \rightarrow \psi \leftrightarrow \varphi \rightarrow \chi) \)
mpbi l0 _