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  ax10lem4  1881  ax12  2095  rgen2a  2609  rspct  2877  po2nr  4327  somo  4348  ordelord  4414  tz7.7  4418  onint  4586  funssres  5294  2elresin  5355  dffv2  5592  f1imass  5788  riotasv2dOLD  6350  onfununi  6358  smoel  6377  tfrlem11  6404  tfr3  6415  omass  6578  nnmass  6622  sbthlem1  6971  php  7045  inf3lem2  7330  cardne  7598  dfac2  7757  indpi  8531  genpcd  8630  ltexprlem7  8666  addcanpr  8670  reclem4pr  8674  suplem2pr  8677  sup2  9710  nnunb  9961  uzwo  10281  uzwoOLD  10282  xrub  10630  grpid  14517  lsmcss  16592  uniopn  16643  fclsss1  17717  fclsss2  17718  grpoid  20890  spansncvi  22231  pjnormssi  22748  sumdmdlem2  22999  trpredrec  24241  wfrlem12  24267  wfrlem14  24269  frrlem11  24293  sltval2  24310  nobndup  24354  nobnddown  24355  meran1  24850  oriso  25214  tartarmap  25888  afv0nbfvbi  28014  ee223  28406  eel2122old  28497  ax10lem18ALT  29124  hlhilhillem  32153
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator