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  ax12  1888  ax10lem4  1894  ax12from12o  2108  rgen2a  2622  rspct  2890  po2nr  4343  somo  4364  ordelord  4430  tz7.7  4434  onint  4602  funssres  5310  2elresin  5371  dffv2  5608  f1imass  5804  riotasv2dOLD  6366  onfununi  6374  smoel  6393  tfrlem11  6420  tfr3  6431  omass  6594  nnmass  6638  sbthlem1  6987  php  7061  inf3lem2  7346  cardne  7614  dfac2  7773  indpi  8547  genpcd  8646  ltexprlem7  8682  addcanpr  8686  reclem4pr  8690  suplem2pr  8693  sup2  9726  nnunb  9977  uzwo  10297  uzwoOLD  10298  xrub  10646  grpid  14533  lsmcss  16608  uniopn  16659  fclsss1  17733  fclsss2  17734  grpoid  20906  spansncvi  22247  pjnormssi  22764  sumdmdlem2  23015  trpredrec  24311  wfrlem12  24337  wfrlem14  24339  frrlem11  24363  sltval2  24380  nobndup  24424  nobnddown  24425  meran1  24921  oriso  25316  tartarmap  25990  afv0nbfvbi  28118  ee223  28710  eel2122old  28804  ax10lem4NEW7  29447  ax10lem18ALT  29746  hlhilhillem  32775
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator