Theorem syl3anr2

A syllogism inference. (Contributed by NM, 1-Aug-2007.) (Proof shortened by Wolf Lammen, 27-Jun-2022.)

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