Theorem baibr

Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)

Hypothesis
baib.1
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \)
Conclusion
\( \vdash \psi \rightarrow (\chi \leftrightarrow \varphi) \)
Proof
baib.1
baib _
bicomd _