Theorem rbaib

Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)

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