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  6970  fiintim  7238  eqinfti  7361  finomni  7481  frecuzrdgrclt  10867  seq3coll  11310  swrdswrd  11493  swrdccatin1  11513  swrdccatin2  11517  fprodsplitsn  12419  nninfctlemfo  12836  unct  13385  isnzr2  14575  dvcnp2cntop  15891  fsumdvdsmul  16246  perfectlem2  16261  upgrwlkcompim  16769  wlkv0  16776  trlsegvdeglem1  16867