Theorem simpl2im

Implication from an eliminated conjunct implied by the antecedent. (Contributed by BJ/AV, 5-Apr-2021.) (Proof shortened by Wolf Lammen, 26-Mar-2022.)

Hypotheses
simpl2im.1
\( \vdash \varphi \rightarrow \psi \wedge \chi \)
simpl2im.2
\( \vdash \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
simpl2im.1
\( \vdash \varphi \rightarrow \psi \wedge \chi \)
l1
simprd _
\( \vdash \varphi \rightarrow \chi \)
simpl2im.2
\( \vdash \chi \rightarrow \theta \)
syl l1 _