Theorem pm5.74da

Distribution of implication over biconditional (deduction form). Variant of pm5.74d. (Contributed by NM, 4-May-2007.)

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