Theorem baib

Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)

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