Theorem pm5.32d

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

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