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

Theorem pm2.43d 49
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 23 . 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  105  rgen2aOLD  2834  rspct  3155  po2nr  4759  somo  4780  ordelord  5434  tz7.7  5438  funssres  5611  2elresin  5675  dffv2  5924  f1imass  6155  onint  6615  wfrlem12  7034  wfrlem14  7036  onfununi  7047  smoel  7066  tfrlem11  7093  tfr3  7104  omass  7268  nnmass  7312  sbthlem1  7667  php  7741  inf3lem2  8081  cardne  8380  dfac2  8545  indpi  9317  genpcd  9416  ltexprlem7  9452  addcanpr  9456  reclem4pr  9460  suplem2pr  9463  sup2  10541  nnunb  10834  uzwo  11192  xrub  11558  grpid  16411  lsmcss  19023  uniopn  19700  fclsss1  20817  fclsss2  20818  0clwlk  25194  frg2wot1  25486  grpoid  25652  spansncvi  26997  pjnormssi  27513  sumdmdlem2  27764  trpredrec  30065  frrlem11  30112  sltval2  30129  nobndup  30173  nobnddown  30174  meran1  30656  heicant  31434  ax13fromc9  31941  hlhilhillem  34996  ee223  36457  eel2122old  36550  afv0nbfvbi  37617  usgedgvadf1lem2  38056  usgedgvadf1ALTlem2  38059
  Copyright terms: Public domain W3C validator