Theorem syl3an3

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

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