Theorem biancomi

Commuting conjunction in a biconditional. (Contributed by Peter Mazsa, 17-Jun-2018.)

Hypothesis
biancomi.1
\( \vdash \varphi \leftrightarrow \chi \wedge \psi \)
Conclusion
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \)
Proof
l0
biancomi.1
\( \vdash \varphi \leftrightarrow \chi \wedge \psi \)
ancom
\( \vdash \psi \wedge \chi \leftrightarrow \chi \wedge \psi \)
bitr4i l0 _