Metamath Proof Explorer


Theorem simpl2im

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

Ref Expression
Hypotheses simpl2im.1 φ ψ χ
simpl2im.2 χ θ
Assertion simpl2im φ θ

Proof

Step Hyp Ref Expression
1 simpl2im.1 φ ψ χ
2 simpl2im.2 χ θ
3 1 simprd φ χ
4 3 2 syl φ θ