Theorem sylan2d

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

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