Theorem impel 485

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 34	. 2 |- ( ph -> ( th -> ch ) )
4	3	imp 445	1 |- ( ( ph /\ th ) -> ch )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  equs5e  2349  elabgt  3347  mob2  3386  ssn0rex  3936  reusv2lem2  4869  copsex2t  4957  trssord  5740  trsuc  5810  ectocld  7814  fiint  8237  eqinf  8390  lcmfunsnlem2lem2  15352  tnggrpr  22459  wlkv0  26547  wlkp1lem1  26570  wlkpwwlkf1ouspgr  26765  wspniunwspnon  26819  wwlksext2clwwlk  26924  trlsegvdeglem1  27080  frcond4  27134  noresle  31846  bj-restpw  33045  cover2  33508  setindtr  37591  climxlim2lem  40071  lighneallem4  41527  proththd  41531