Theorem anbi12i

Conjoin both sides of two equivalences. (Contributed by NM, 12-Mar-1993.)

Hypotheses
anbi12.1
\( \vdash \varphi \leftrightarrow \psi \)
anbi12.2
\( \vdash \chi \leftrightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \chi \leftrightarrow \psi \wedge \theta \)
Proof
anbi12.2
l1
anbi2i _
\( \vdash \varphi \wedge \chi \leftrightarrow \varphi \wedge \theta \)
anbi12.1
\( \vdash \varphi \leftrightarrow \psi \)
bianbi l1 _