Theorem 3anim123d

Deduction joining 3 implications to form implication of conjunctions. (Contributed by NM, 24-Feb-2005.)

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