Theorem anbi1ci

Variant of anbi1i with commutation. (Contributed by Peter Mazsa, 7-Mar-2020.)

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