Theorem
rbaibd
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 \theta \rightarrow (\psi \leftrightarrow \chi) \)
Proof
baibd.1
biancomd
_
baibd
_
This is the content in the right pane.