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 )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is referenced by:  pm4.55dc  947  mapsnd  6923  fiintim  7191  eqinfti  7311  finomni  7431  frecuzrdgrclt  10777  seq3coll  11214  swrdswrd  11397  swrdccatin1  11417  swrdccatin2  11421  fprodsplitsn  12319  nninfctlemfo  12736  unct  13193  isnzr2  14329  dvcnp2cntop  15564  fsumdvdsmul  15859  perfectlem2  15868  upgrwlkcompim  16357  wlkv0  16364  trlsegvdeglem1  16455