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

Theorem pm2.43d 48
Description: Deduction absorbing redundant antecedent. (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 42 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  103  ax13fromc9  2221  rgen2aOLD  2871  rspct  3189  po2nr  4803  somo  4824  ordelord  4890  tz7.7  4894  funssres  5618  2elresin  5682  dffv2  5931  f1imass  6157  onint  6615  onfununi  7014  smoel  7033  tfrlem11  7059  tfr3  7070  omass  7231  nnmass  7275  sbthlem1  7629  php  7703  inf3lem2  8049  cardne  8349  dfac2  8514  indpi  9288  genpcd  9387  ltexprlem7  9423  addcanpr  9427  reclem4pr  9431  suplem2pr  9434  sup2  10506  nnunb  10798  uzwo  11155  uzwoOLD  11156  xrub  11514  grpid  16064  lsmcss  18701  uniopn  19384  fclsss1  20501  fclsss2  20502  0clwlk  24743  frg2wot1  25035  grpoid  25203  spansncvi  26548  pjnormssi  27065  sumdmdlem2  27316  trpredrec  29297  wfrlem12  29330  wfrlem14  29332  frrlem11  29375  sltval2  29392  nobndup  29436  nobnddown  29437  meran1  29852  heicant  30025  afv0nbfvbi  32190  usgedgvadf1lem2  32368  usgedgvadf1ALTlem2  32371  ee223  33288  eel2122old  33381  hlhilhillem  37565
  Copyright terms: Public domain W3C validator