Theorem pm5.74rd

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

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