MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.43a Structured version   Unicode version

Theorem pm2.43a 49
Description: Inference absorbing redundant antecedent. (Contributed by NM, 7-Nov-1995.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.)
Hypothesis
Ref Expression
pm2.43a.1  |-  ( ps 
->  ( ph  ->  ( ps  ->  ch ) ) )
Assertion
Ref Expression
pm2.43a  |-  ( ps 
->  ( ph  ->  ch ) )

Proof of Theorem pm2.43a
StepHypRef Expression
1 id 22 . 2  |-  ( ps 
->  ps )
2 pm2.43a.1 . 2  |-  ( ps 
->  ( ph  ->  ( ps  ->  ch ) ) )
31, 2mpid 41 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  pm2.43b  50  rspc  3208  intss1  4297  fvopab3ig  5946  suppimacnv  6912  odi  7228  nndi  7272  inf3lem2  8045  pr2ne  8382  zorn2lem7  8881  uzind2  10952  uzindOLD  10954  ssfzo12  11872  elfznelfzo  11882  injresinj  11893  suppssfz  12067  sqlecan  12241  brfi1uzind  12497  cramerimplem2  18969  fiinopn  19193  bwthOLD  19693  usgraedg4  24079  wlkdvspthlem  24301  usgrcyclnl1  24332  3cyclfrgrarn1  24704  vdn0frgrav2  24716  vdn1frgrav2  24718  vdgn1frgrav2  24719  numclwlk1lem2foa  24784  dvrunz  25127  afveu  31721  lindslinindsimp2  32154  ee223  32509
  Copyright terms: Public domain W3C validator