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

Theorem pm2.43d 46
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 20 . 2  |-  ( ps 
->  ps )
2 pm2.43d.1 . 2  |-  ( ph  ->  ( ps  ->  ( ps  ->  ch ) ) )
31, 2mpdi 40 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  loolin  97  ax12-OLD  1966  ax10lem4  1973  ax12from12o  2183  rgen2a  2708  rspct  2981  po2nr  4450  somo  4471  ordelord  4537  tz7.7  4541  onint  4708  funssres  5426  2elresin  5489  dffv2  5728  f1imass  5942  riotasv2dOLD  6524  onfununi  6532  smoel  6551  tfrlem11  6578  tfr3  6589  omass  6752  nnmass  6796  sbthlem1  7146  php  7220  inf3lem2  7510  cardne  7778  dfac2  7937  indpi  8710  genpcd  8809  ltexprlem7  8845  addcanpr  8849  reclem4pr  8853  suplem2pr  8856  sup2  9889  nnunb  10142  uzwo  10464  uzwoOLD  10465  xrub  10815  grpid  14760  lsmcss  16835  uniopn  16886  fclsss1  17968  fclsss2  17969  grpoid  21652  spansncvi  22995  pjnormssi  23512  sumdmdlem2  23763  trpredrec  25258  wfrlem12  25284  wfrlem14  25286  frrlem11  25310  sltval2  25327  nobndup  25371  nobnddown  25372  meran1  25868  afv0nbfvbi  27677  ee223  28069  eel2122old  28162  ax10lem4NEW7  28802  ax10lem18ALT  29100  hlhilhillem  32129
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator