Theorem 3orim123d

Deduction joining 3 implications to form implication of disjunctions. (Contributed by NM, 4-Apr-1997.)

Hypotheses
3anim123d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
3anim123d.2
\( \vdash \varphi \rightarrow \theta \rightarrow \tau \)
3anim123d.3
\( \vdash \varphi \rightarrow \eta \rightarrow \zeta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \vee \theta \vee \eta \rightarrow \chi \vee \tau \vee \zeta \)
Proof
l0
3anim123d.1
3anim123d.2
l2
orim12d l0 _
3anim123d.3
l4
orim12d l2 _
\( \vdash \varphi \rightarrow \psi \vee \theta \vee \eta \rightarrow \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 \)
3imtr4g l4 l5 _