Theorem sylani

A syllogism inference. (Contributed by NM, 2-May-1996.)

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