Theorem 3anbi123i

Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994.)

Hypotheses
bi3.1
\( \vdash \varphi \leftrightarrow \psi \)
bi3.2
\( \vdash \chi \leftrightarrow \theta \)
bi3.3
\( \vdash \tau \leftrightarrow \eta \)
Conclusion
\( \vdash \varphi \wedge \chi \wedge \tau \leftrightarrow \psi \wedge \theta \wedge \eta \)
Proof
l0
bi3.1
bi3.2
l2
anbi12i l0 _
bi3.3
l4
anbi12i l2 _
\( \vdash \varphi \wedge \chi \wedge \tau \leftrightarrow \psi \wedge \theta \wedge \eta \)
l5
df-3an
\( \vdash \varphi \wedge \chi \wedge \tau \leftrightarrow \varphi \wedge \chi \wedge \tau \)
df-3an
\( \vdash \psi \wedge \theta \wedge \eta \leftrightarrow \psi \wedge \theta \wedge \eta \)
3bitr4i l4 l5 _