Theorem syl3anl1

A syllogism inference. (Contributed by NM, 24-Feb-2005.)

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