Theorem syl3anl

A triple syllogism inference. (Contributed by NM, 24-Dec-2006.)

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