Theorem pm5.32rd

Distribution of implication over biconditional (deduction form). (Contributed by NM, 25-Dec-2004.)

Hypothesis
pm5.32d.1
\( \vdash \varphi \rightarrow \psi \rightarrow (\chi \leftrightarrow \theta) \)
Conclusion
\( \vdash \varphi \rightarrow (\chi \wedge \psi \leftrightarrow \theta \wedge \psi) \)
Proof
pm5.32d.1
l1
pm5.32d _
\( \vdash \varphi \rightarrow (\psi \wedge \chi \leftrightarrow \psi \wedge \theta) \)
l2
ancom
\( \vdash \chi \wedge \psi \leftrightarrow \psi \wedge \chi \)
ancom
\( \vdash \theta \wedge \psi \leftrightarrow \psi \wedge \theta \)
3bitr4g l1 l2 _