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

Theorem pm2.43d 47
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 21 . 2  |-  ( ps 
->  ps )
2 pm2.43d.1 . 2  |-  ( ph  ->  ( ps  ->  ( ps  ->  ch ) ) )
31, 2mpdi 41 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  loolin  98  ax12OLD  2021  ax10lem4OLD  2031  ax12from12o  2235  rgen2a  2774  rspct  3047  po2nr  4518  somo  4539  ordelord  4605  tz7.7  4609  onint  4777  funssres  5495  2elresin  5558  dffv2  5798  f1imass  6012  riotasv2dOLD  6597  onfununi  6605  smoel  6624  tfrlem11  6651  tfr3  6662  omass  6825  nnmass  6869  sbthlem1  7219  php  7293  inf3lem2  7586  cardne  7854  dfac2  8013  indpi  8786  genpcd  8885  ltexprlem7  8921  addcanpr  8925  reclem4pr  8929  suplem2pr  8932  sup2  9966  nnunb  10219  uzwo  10541  uzwoOLD  10542  xrub  10892  grpid  14842  lsmcss  16921  uniopn  16972  fclsss1  18056  fclsss2  18057  grpoid  21813  spansncvi  23156  pjnormssi  23673  sumdmdlem2  23924  trpredrec  25518  wfrlem12  25551  wfrlem14  25553  frrlem11  25596  sltval2  25613  nobndup  25657  nobnddown  25658  meran1  26163  afv0nbfvbi  27993  frg2wot1  28508  ee223  28797  eel2122old  28890  ax10lem4NEW7  29533  hlhilhillem  32823
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator