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

Theorem pm2.43d 50
Description: Deduction absorbing redundant antecedent. Deduction associated with pm2.43 53 and pm2.43i 49. (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 43 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  106  rgen2aOLD  2816  rspct  3143  po2nr  4768  somo  4789  ordelord  5445  tz7.7  5449  funssres  5622  2elresin  5687  dffv2  5938  f1imass  6165  onint  6622  wfrlem12  7047  wfrlem14  7049  onfununi  7060  smoel  7079  tfrlem11  7106  tfr3  7117  omass  7281  nnmass  7325  sbthlem1  7682  php  7756  inf3lem2  8134  cardne  8399  dfac2  8561  indpi  9332  genpcd  9431  ltexprlem7  9467  addcanpr  9471  reclem4pr  9475  suplem2pr  9478  sup2  10565  nnunb  10865  uzwo  11222  xrub  11597  grpid  16701  lsmcss  19255  uniopn  19927  fclsss1  21037  fclsss2  21038  0clwlk  25493  frg2wot1  25785  grpoid  25951  spansncvi  27305  pjnormssi  27821  sumdmdlem2  28072  trpredrec  30479  frrlem11  30526  sltval2  30543  nobndup  30589  nobnddown  30590  meran1  31071  poimirlem31  31971  heicant  31975  ax13fromc9  32476  hlhilhillem  35531  ee223  37013  eel2122old  37103  afv0nbfvbi  38653  usgedgvadf1lem2  39779  usgedgvadf1ALTlem2  39782
  Copyright terms: Public domain W3C validator