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  3067  intss1  4143  fvopab3ig  5771  suppimacnv  6701  odi  7018  nndi  7062  inf3lem2  7835  pr2ne  8172  zorn2lem7  8671  uzind2  10734  uzindOLD  10736  ssfzo12  11620  elfznelfzo  11630  injresinj  11639  sqlecan  11972  brfi1uzind  12219  cramerimplem2  18490  fiinopn  18514  bwthOLD  19014  usgraedg4  23305  wlkdvspthlem  23506  usgrcyclnl1  23526  dvrunz  23920  afveu  30059  3cyclfrgrarn1  30604  vdn0frgrav2  30616  vdn1frgrav2  30618  vdgn1frgrav2  30619  numclwlk1lem2foa  30684  suppssfz  30786  lindslinindsimp2  30997  ee223  31356
  Copyright terms: Public domain W3C validator