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

Theorem pm2.43d 48
Description: Deduction absorbing redundant antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.)
Hypothesis
Ref Expression
pm2.43d.1  |-  ( ph  ->  ( ps  ->  ( ps  ->  ch ) ) )
Assertion
Ref Expression
pm2.43d  |-  ( ph  ->  ( ps  ->  ch ) )

Proof of Theorem pm2.43d
StepHypRef Expression
1 id 22 . 2  |-  ( ps 
->  ps )
2 pm2.43d.1 . 2  |-  ( ph  ->  ( ps  ->  ( ps  ->  ch ) ) )
31, 2mpdi 42 1  |-  ( ph  ->  ( ps  ->  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:  loolin  103  ax13fromc9  2228  rgen2aOLD  2892  rspct  3207  po2nr  4813  somo  4834  ordelord  4900  tz7.7  4904  funssres  5626  2elresin  5690  dffv2  5938  f1imass  6158  onint  6608  onfununi  7009  smoel  7028  tfrlem11  7054  tfr3  7065  omass  7226  nnmass  7270  sbthlem1  7624  php  7698  inf3lem2  8042  cardne  8342  dfac2  8507  indpi  9281  genpcd  9380  ltexprlem7  9416  addcanpr  9420  reclem4pr  9424  suplem2pr  9427  sup2  10495  nnunb  10787  uzwo  11140  uzwoOLD  11141  xrub  11499  grpid  15886  lsmcss  18490  uniopn  19173  fclsss1  20258  fclsss2  20259  0clwlk  24441  frg2wot1  24734  grpoid  24901  spansncvi  26246  pjnormssi  26763  sumdmdlem2  27014  trpredrec  28898  wfrlem12  28931  wfrlem14  28933  frrlem11  28976  sltval2  28993  nobndup  29037  nobnddown  29038  meran1  29453  heicant  29626  afv0nbfvbi  31703  usgedgvadf1lem2  31883  usgedgvadf1ALTlem2  31886  ee223  32500  eel2122old  32593  hlhilhillem  36760
  Copyright terms: Public domain W3C validator