Metamath Proof Explorer


Theorem impel

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

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

Proof

Step Hyp Ref Expression
1 impel.1 φ ψ χ
2 impel.2 θ ψ
3 2 1 syl5 φ θ χ
4 3 imp φ θ χ