Theorem pm5.74d

Distribution of implication over biconditional (deduction form). (Contributed by NM, 21-Mar-1996.)

Hypothesis
pm5.74d.1
\( \vdash \varphi \rightarrow \psi \rightarrow (\chi \leftrightarrow \theta) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \rightarrow \chi \leftrightarrow \psi \rightarrow \theta) \)
Proof
l0
pm5.74d.1
\( \vdash \varphi \rightarrow \psi \rightarrow (\chi \leftrightarrow \theta) \)
pm5.74
\( \vdash \psi \rightarrow (\chi \leftrightarrow \theta) \leftrightarrow (\psi \rightarrow \chi \leftrightarrow \psi \rightarrow \theta) \)
sylib l0 _