Theorem sylan9r

Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.)

Hypotheses
sylan9r.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
sylan9r.2
\( \vdash \theta \rightarrow \chi \rightarrow \tau \)
Conclusion
\( \vdash \theta \wedge \varphi \rightarrow \psi \rightarrow \tau \)
Proof
l0
sylan9r.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
sylan9r.2
\( \vdash \theta \rightarrow \chi \rightarrow \tau \)
syl9r l0 _
imp _