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

Theorem pm2.43d 51
Description: Deduction absorbing redundant antecedent. Deduction associated with pm2.43 54 and pm2.43i 50. (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 23 . 2  |-  ( ps 
->  ps )
2 pm2.43d.1 . 2  |-  ( ph  ->  ( ps  ->  ( ps  ->  ch ) ) )
31, 2mpdi 44 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  107  rgen2aOLD  2854  rspct  3176  po2nr  4785  somo  4806  ordelord  5462  tz7.7  5466  funssres  5639  2elresin  5703  dffv2  5952  f1imass  6178  onint  6634  wfrlem12  7053  wfrlem14  7055  onfununi  7066  smoel  7085  tfrlem11  7112  tfr3  7123  omass  7287  nnmass  7331  sbthlem1  7686  php  7760  inf3lem2  8138  cardne  8402  dfac2  8563  indpi  9334  genpcd  9433  ltexprlem7  9469  addcanpr  9473  reclem4pr  9477  suplem2pr  9480  sup2  10567  nnunb  10867  uzwo  11224  xrub  11599  grpid  16694  lsmcss  19247  uniopn  19919  fclsss1  21029  fclsss2  21030  0clwlk  25485  frg2wot1  25777  grpoid  25943  spansncvi  27297  pjnormssi  27813  sumdmdlem2  28064  trpredrec  30480  frrlem11  30527  sltval2  30544  nobndup  30588  nobnddown  30589  meran1  31070  poimirlem31  31891  heicant  31895  ax13fromc9  32401  hlhilhillem  35456  ee223  36878  eel2122old  36970  afv0nbfvbi  38371  usgedgvadf1lem2  39030  usgedgvadf1ALTlem2  39033
  Copyright terms: Public domain W3C validator