Theorem syl8

A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 1-Aug-1994.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)

Hypotheses
syl8.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
syl8.2
\( \vdash \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \tau \)
Proof
l0
syl8.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
syl8.2
a1i _
\( \vdash \varphi \rightarrow \theta \rightarrow \tau \)
syl6d l0 _