Theorem syl3an

A triple syllogism inference. (Contributed by NM, 13-May-2004.)

Hypotheses
syl3an.1
\( \vdash \varphi \rightarrow \psi \)
syl3an.2
\( \vdash \chi \rightarrow \theta \)
syl3an.3
\( \vdash \tau \rightarrow \eta \)
syl3an.4
\( \vdash \psi \wedge \theta \wedge \eta \rightarrow \zeta \)
Conclusion
\( \vdash \varphi \wedge \chi \wedge \tau \rightarrow \zeta \)
Proof
l0
syl3an.1
l1
syl3an.2
syl3an.3
l3
3anim123i l0 l1 _
\( \vdash \varphi \wedge \chi \wedge \tau \rightarrow \psi \wedge \theta \wedge \eta \)
syl3an.4
\( \vdash \psi \wedge \theta \wedge \eta \rightarrow \zeta \)
syl l3 _