Theorem 3anbi123d

Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.)

Hypotheses
bi3d.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
bi3d.2
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \tau) \)
bi3d.3
\( \vdash \varphi \rightarrow (\eta \leftrightarrow \zeta) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \wedge \theta \wedge \eta \leftrightarrow \chi \wedge \tau \wedge \zeta) \)
Proof
l0
bi3d.1
bi3d.2
l2
anbi12d l0 _
bi3d.3
l4
anbi12d l2 _
\( \vdash \varphi \rightarrow (\psi \wedge \theta \wedge \eta \leftrightarrow \chi \wedge \tau \wedge \zeta) \)
l5
df-3an
\( \vdash \psi \wedge \theta \wedge \eta \leftrightarrow \psi \wedge \theta \wedge \eta \)
df-3an
\( \vdash \chi \wedge \tau \wedge \zeta \leftrightarrow \chi \wedge \tau \wedge \zeta \)
3bitr4g l4 l5 _