Theorem rbaibr

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 (\psi \leftrightarrow \varphi) \)
Proof
baib.1
biancomi _
baibr _