Theorem syl3anl2

A syllogism inference. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 27-Jun-2022.)

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