Theorem syl3an2

A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)

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