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  2206  rgen2a  2782  rspct  3066  po2nr  4654  somo  4675  ordelord  4741  tz7.7  4745  funssres  5458  2elresin  5522  dffv2  5764  f1imass  5977  onint  6406  onfununi  6802  smoel  6821  tfrlem11  6847  tfr3  6858  omass  7019  nnmass  7063  sbthlem1  7421  php  7495  inf3lem2  7835  cardne  8135  dfac2  8300  indpi  9076  genpcd  9175  ltexprlem7  9211  addcanpr  9215  reclem4pr  9219  suplem2pr  9222  sup2  10286  nnunb  10575  uzwo  10917  uzwoOLD  10918  xrub  11274  grpid  15573  lsmcss  18117  uniopn  18510  fclsss1  19595  fclsss2  19596  grpoid  23710  spansncvi  25055  pjnormssi  25572  sumdmdlem2  25823  trpredrec  27702  wfrlem12  27735  wfrlem14  27737  frrlem11  27780  sltval2  27797  nobndup  27841  nobnddown  27842  meran1  28257  heicant  28426  afv0nbfvbi  30057  0clwlk  30428  frg2wot1  30650  ee223  31356  eel2122old  31449  hlhilhillem  35608
  Copyright terms: Public domain W3C validator