Theorem sylanl1

A syllogism inference. (Contributed by NM, 10-Mar-2005.)

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