Theorem pm5.32ri

Distribution of implication over biconditional (inference form). (Contributed by NM, 12-Mar-1995.)

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