Theorem impel

An inference for implication elimination. (Contributed by Giovanni Mascellani, 23-May-2019.) (Proof shortened by Wolf Lammen, 2-Sep-2020.)

Hypotheses
impel.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
impel.2
\( \vdash \theta \rightarrow \psi \)
Conclusion
\( \vdash \varphi \wedge \theta \rightarrow \chi \)
Proof
l0
impel.2
\( \vdash \theta \rightarrow \psi \)
impel.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
syl5 l0 _
imp _