Theorem syli

Syllogism inference with common nested antecedent. (Contributed by NM, 4-Nov-2004.)

Hypotheses
syli.1
\( \vdash \psi \rightarrow \varphi \rightarrow \chi \)
syli.2
\( \vdash \chi \rightarrow \varphi \rightarrow \theta \)
Conclusion
\( \vdash \psi \rightarrow \varphi \rightarrow \theta \)
Proof
l0
syli.1
\( \vdash \psi \rightarrow \varphi \rightarrow \chi \)
syli.2
com12 _
\( \vdash \varphi \rightarrow \chi \rightarrow \theta \)
sylcom l0 _