Theorem sylan2i

A syllogism inference. (Contributed by NM, 1-Aug-1994.)

Hypotheses
sylan2i.1
\( \vdash \varphi \rightarrow \theta \)
sylan2i.2
\( \vdash \psi \rightarrow \chi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \psi \rightarrow \chi \wedge \varphi \rightarrow \tau \)
Proof
sylan2i.1
l1
a1i _
\( \vdash \psi \rightarrow \varphi \rightarrow \theta \)
sylan2i.2
\( \vdash \psi \rightarrow \chi \wedge \theta \rightarrow \tau \)
sylan2d l1 _