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
Assertion
Ref Expression
pm2.43d

Proof of Theorem pm2.43d
StepHypRef Expression
1 id 19 . 2
2 pm2.43d.1 . 2
31, 2mpdi 38 1
 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  24312  wfrlem12  24338  wfrlem14  24340  frrlem11  24364  sltval2  24381  nobndup  24425  nobnddown  24426  meran1  24922  oriso  25317  tartarmap  25991  afv0nbfvbi  28119  ee223  28711  eel2122old  28805  ax10lem4NEW7  29448  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