Theorem anbi2ci

Variant of anbi2i with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)

Hypothesis
anbi.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \varphi \wedge \chi \leftrightarrow \chi \wedge \psi \)
Proof
anbi.1
anbi1i _
biancomi _