Theorem sylan

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

Hypotheses
sylan.1
\( \vdash \varphi \rightarrow \psi \)
sylan.2
\( \vdash \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \chi \rightarrow \theta \)
Proof
l0
sylan.1
\( \vdash \varphi \rightarrow \psi \)
sylan.2
expcom _
\( \vdash \chi \rightarrow \psi \rightarrow \theta \)
mpan9 l0 _