Theorem sylan9

Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)

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