Theorem sylanl2

A syllogism inference. (Contributed by NM, 1-Jan-2005.)

Hypotheses
sylanl2.1
\( \vdash \varphi \rightarrow \chi \)
sylanl2.2
\( \vdash \psi \wedge \chi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \psi \wedge \varphi \wedge \theta \rightarrow \tau \)
Proof
sylanl2.1
l1
adantl _
\( \vdash \psi \wedge \varphi \rightarrow \chi \)
sylanl2.2
\( \vdash \psi \wedge \chi \wedge \theta \rightarrow \tau \)
syldanl l1 _