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  7360  finomni  7480  frecuzrdgrclt  10865  seq3coll  11308  swrdswrd  11491  swrdccatin1  11511  swrdccatin2  11515  fprodsplitsn  12416  nninfctlemfo  12833  unct  13382  isnzr2  14540  dvcnp2cntop  15849  fsumdvdsmul  16186  perfectlem2  16198  upgrwlkcompim  16701  wlkv0  16708  trlsegvdeglem1  16799