Theorem 3orbi123d

Deduction joining 3 equivalences to form equivalence of disjunctions. (Contributed by NM, 20-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 \vee \theta \vee \eta \leftrightarrow \chi \vee \tau \vee \zeta) \)
Proof
l0
bi3d.1
bi3d.2
l2
orbi12d l0 _
bi3d.3
l4
orbi12d l2 _
\( \vdash \varphi \rightarrow (\psi \vee \theta \vee \eta \leftrightarrow \chi \vee \tau \vee \zeta) \)
l5
df-3or
\( \vdash \psi \vee \theta \vee \eta \leftrightarrow \psi \vee \theta \vee \eta \)
df-3or
\( \vdash \chi \vee \tau \vee \zeta \leftrightarrow \chi \vee \tau \vee \zeta \)
3bitr4g l4 l5 _