Theorem syl3anl3

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

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