Theorem syl3an1

A syllogism inference. (Contributed by NM, 22-Aug-1995.)

Hypotheses
syl3an1.1
\( \vdash \varphi \rightarrow \psi \)
syl3an1.2
\( \vdash \psi \wedge \chi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \wedge \chi \wedge \theta \rightarrow \tau \)
Proof
syl3an1.1
l1
3anim1i _
\( \vdash \varphi \wedge \chi \wedge \theta \rightarrow \psi \wedge \chi \wedge \theta \)
syl3an1.2
\( \vdash \psi \wedge \chi \wedge \theta \rightarrow \tau \)
syl l1 _