Theorem pm5.32da

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

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