Theorem syl3anr1

A syllogism inference. (Contributed by NM, 31-Jul-2007.)

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