Theorem baibd

Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)

Hypothesis
baibd.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi \wedge \theta) \)
Conclusion
\( \vdash \varphi \wedge \chi \rightarrow (\psi \leftrightarrow \theta) \)
Proof
l0
baibd.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi \wedge \theta) \)
ibar
bicomd _
\( \vdash \chi \rightarrow (\chi \wedge \theta \leftrightarrow \theta) \)
sylan9bb l0 _