Theorem syl3anr3

A syllogism inference. (Contributed by NM, 23-Aug-2007.)

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