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  ax12OLD  1986  ax10lem4OLD  1996  ax12from12o  2206  rgen2a  2732  rspct  3005  po2nr  4476  somo  4497  ordelord  4563  tz7.7  4567  onint  4734  funssres  5452  2elresin  5515  dffv2  5755  f1imass  5969  riotasv2dOLD  6554  onfununi  6562  smoel  6581  tfrlem11  6608  tfr3  6619  omass  6782  nnmass  6826  sbthlem1  7176  php  7250  inf3lem2  7540  cardne  7808  dfac2  7967  indpi  8740  genpcd  8839  ltexprlem7  8875  addcanpr  8879  reclem4pr  8883  suplem2pr  8886  sup2  9920  nnunb  10173  uzwo  10495  uzwoOLD  10496  xrub  10846  grpid  14795  lsmcss  16874  uniopn  16925  fclsss1  18007  fclsss2  18008  grpoid  21764  spansncvi  23107  pjnormssi  23624  sumdmdlem2  23875  trpredrec  25455  wfrlem12  25481  wfrlem14  25483  frrlem11  25507  sltval2  25524  nobndup  25568  nobnddown  25569  meran1  26065  afv0nbfvbi  27882  frg2wot1  28160  ee223  28444  eel2122old  28537  ax10lem4NEW7  29177  hlhilhillem  32446
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator