Theorem pm5.74ri

Distribution of implication over biconditional (reverse inference form). (Contributed by NM, 1-Aug-1994.)

Hypothesis
pm5.74ri.1
\( \vdash \varphi \rightarrow \psi \leftrightarrow \varphi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Proof
l0
pm5.74ri.1
\( \vdash \varphi \rightarrow \psi \leftrightarrow \varphi \rightarrow \chi \)
pm5.74
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \leftrightarrow (\varphi \rightarrow \psi \leftrightarrow \varphi \rightarrow \chi) \)
mpbir l0 _