Theorem syl7

A syllogism rule of inference. The first premise is used to replace the third antecedent of the second premise. (Contributed by NM, 12-Jan-1993.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)

Hypotheses
syl7.1
\( \vdash \varphi \rightarrow \psi \)
syl7.2
\( \vdash \chi \rightarrow \theta \rightarrow \psi \rightarrow \tau \)
Conclusion
\( \vdash \chi \rightarrow \theta \rightarrow \varphi \rightarrow \tau \)
Proof
syl7.1
l1
a1i _
\( \vdash \chi \rightarrow \varphi \rightarrow \psi \)
syl7.2
\( \vdash \chi \rightarrow \theta \rightarrow \psi \rightarrow \tau \)
syl5d l1 _