Theorem syld

Syllogism deduction. Deduction associated with syl. See [conventions] for the meaning of "associated deduction" or "deduction form". (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mel L. O'Cat, 19-Feb-2008.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)

Hypotheses
syld.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
syld.2
\( \vdash \varphi \rightarrow \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \)
Proof
l0
syld.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
syld.2
a1d _
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
mpdd l0 _