Theorem impel 280

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

Hypotheses

Ref	Expression
impel.1	|- ( ph -> ( ps -> ch ) )
impel.2	|- ( th -> ps )

Assertion

Ref	Expression
impel	|- ( ( ph /\ th ) -> ch )

Proof of Theorem impel

Step	Hyp	Ref	Expression
1		impel.2	. . 3 |- ( th -> ps )
2		impel.1	. . 3 |- ( ph -> ( ps -> ch ) )
3	1, 2	syl5 32	. 2 |- ( ph -> ( th -> ch ) )
4	3	imp 124	1 |- ( ( ph /\ th ) -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is used by:  pm4.55dc  951  mapsnd  6974  fiintim  7242  eqinfti  7366  finomni  7486  frecuzrdgrclt  10873  seq3coll  11316  swrdswrd  11499  swrdccatin1  11519  swrdccatin2  11523  fprodsplitsn  12425  nninfctlemfo  12842  unct  13391  isnzr2  14600  dvcnp2cntop  15925  fsumdvdsmul  16285  perfectlem2  16300  upgrwlkcompim  16808  wlkv0  16815  trlsegvdeglem1  16906