Theorem syl5

A syllogism rule of inference. The first premise is used to replace the second antecedent of the second premise. (Contributed by NM, 27-Dec-1992.) (Proof shortened by Wolf Lammen, 25-May-2013.)

Hypotheses
syl5.1
\( \vdash \varphi \rightarrow \psi \)
syl5.2
\( \vdash \chi \rightarrow \psi \rightarrow \theta \)
Conclusion
\( \vdash \chi \rightarrow \varphi \rightarrow \theta \)
Proof
l0
syl5.1
\( \vdash \varphi \rightarrow \psi \)
syl5.2
\( \vdash \chi \rightarrow \psi \rightarrow \theta \)
syl5com l0 _
com12 _