Theorem syland

A syllogism deduction. (Contributed by NM, 15-Dec-2004.)

Hypotheses
syland.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
syland.2
\( \vdash \varphi \rightarrow \chi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \psi \wedge \theta \rightarrow \tau \)
Proof
l0
syland.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
syland.2
expd _
\( \vdash \varphi \rightarrow \chi \rightarrow \theta \rightarrow \tau \)
syld l0 _
impd _