Theorem syl9r

A nested syllogism inference with different antecedents. (Contributed by NM, 14-May-1993.)

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