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

Theorem pm2.43d 44
Description: Deduction absorbing redundant antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by 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 19 . 2  |-  ( ps 
->  ps )
2 pm2.43d.1 . 2  |-  ( ph  ->  ( ps  ->  ( ps  ->  ch ) ) )
31, 2mpdi 38 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  loolinALT  95  ax12  1940  ax10lem4  1946  ax12from12o  2161  rgen2a  2685  rspct  2953  po2nr  4409  somo  4430  ordelord  4496  tz7.7  4500  onint  4668  funssres  5376  2elresin  5437  dffv2  5675  f1imass  5875  riotasv2dOLD  6437  onfununi  6445  smoel  6464  tfrlem11  6491  tfr3  6502  omass  6665  nnmass  6709  sbthlem1  7059  php  7133  inf3lem2  7420  cardne  7688  dfac2  7847  indpi  8621  genpcd  8720  ltexprlem7  8756  addcanpr  8760  reclem4pr  8764  suplem2pr  8767  sup2  9800  nnunb  10053  uzwo  10373  uzwoOLD  10374  xrub  10722  grpid  14616  lsmcss  16698  uniopn  16749  fclsss1  17819  fclsss2  17820  grpoid  21002  spansncvi  22345  pjnormssi  22862  sumdmdlem2  23113  trpredrec  24799  wfrlem12  24825  wfrlem14  24827  frrlem11  24851  sltval2  24868  nobndup  24912  nobnddown  24913  meran1  25409  afv0nbfvbi  27339  ee223  28157  eel2122old  28251  ax10lem4NEW7  28894  ax10lem18ALT  29193  hlhilhillem  32222
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator