MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.43d 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
Assertion
Ref Expression
pm2.43d

Proof of Theorem pm2.43d
StepHypRef Expression
1 id 22 . 2
2 pm2.43d.1 . 2
31, 2mpdi 42 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  loolin  103  ax13fromc9  2235  rgen2aOLD  2885  rspct  3203  po2nr  4818  somo  4839  ordelord  4905  tz7.7  4909  funssres  5633  2elresin  5697  dffv2  5946  f1imass  6172  onint  6630  onfununi  7031  smoel  7050  tfrlem11  7076  tfr3  7087  omass  7248  nnmass  7292  sbthlem1  7647  php  7721  inf3lem2  8067  cardne  8367  dfac2  8532  indpi  9306  genpcd  9405  ltexprlem7  9441  addcanpr  9445  reclem4pr  9449  suplem2pr  9452  sup2  10524  nnunb  10816  uzwo  11173  uzwoOLD  11174  xrub  11532  grpid  16085  lsmcss  18723  uniopn  19406  fclsss1  20523  fclsss2  20524  0clwlk  24765  frg2wot1  25057  grpoid  25225  spansncvi  26570  pjnormssi  27087  sumdmdlem2  27338  trpredrec  29321  wfrlem12  29354  wfrlem14  29356  frrlem11  29399  sltval2  29416  nobndup  29460  nobnddown  29461  meran1  29876  heicant  30049  afv0nbfvbi  32236  usgedgvadf1lem2  32414  usgedgvadf1ALTlem2  32417  ee223  33420  eel2122old  33513  hlhilhillem  37690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator