Theorem syl9

A nested syllogism inference with different antecedents. (Contributed by NM, 13-May-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)

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