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  6976  fiintim  7244  eqinfti  7366  finomni  7486  frecuzrdgrclt  10872  seq3coll  11315  swrdswrd  11498  swrdccatin1  11518  swrdccatin2  11522  fprodsplitsn  12424  nninfctlemfo  12841  unct  13390  isnzr2  14599  dvcnp2cntop  15942  fsumdvdsmul  16302  perfectlem2  16317  upgrwlkcompim  16825  wlkv0  16832  trlsegvdeglem1  16923