Theorem sylan2

A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)

Hypotheses
sylan2.1
\( \vdash \varphi \rightarrow \chi \)
sylan2.2
\( \vdash \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \psi \wedge \varphi \rightarrow \theta \)
Proof
sylan2.1
l1
adantl _
\( \vdash \psi \wedge \varphi \rightarrow \chi \)
sylan2.2
\( \vdash \psi \wedge \chi \rightarrow \theta \)
syldan l1 _