Theorem syl6

A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 5-Jan-1993.) (Proof shortened by Wolf Lammen, 30-Jul-2012.)

Hypotheses
syl6.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
syl6.2
\( \vdash \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \)
Proof
l0
syl6.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
syl6.2
a1i _
\( \vdash \psi \rightarrow \chi \rightarrow \theta \)
sylcom l0 _