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 φθχ