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

Theorem negeqd 9302
Description: Equality deduction for negatives. (Contributed by NM, 14-May-1999.)
Hypothesis
Ref Expression
negeqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
negeqd  |-  ( ph  -> 
-u A  =  -u B )

Proof of Theorem negeqd
StepHypRef Expression
1 negeqd.1 . 2  |-  ( ph  ->  A  =  B )
2 negeq 9300 . 2  |-  ( A  =  B  ->  -u A  =  -u B )
31, 2syl 16 1  |-  ( ph  -> 
-u A  =  -u B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   -ucneg 9294
This theorem is referenced by:  negdi  9360  mulneg2  9473  mulm1  9477  ltord2  9558  leord2  9559  eqord2  9560  divneg  9711  div2neg  9739  recgt0  9856  infmsup  9988  supminf  10565  modcyc2  11279  monoord2  11356  expval  11386  discr  11518  reneg  11932  imneg  11940  cjcj  11947  cjneg  11954  sqeqd  11973  fsumtscopo2  12584  infcvgaux1i  12638  infcvgaux2i  12639  sinneg  12749  tanneg  12751  sincossq  12779  odd2np1  12910  oexpneg  12913  modgcd  13038  pcneg  13249  mulgval  14894  mulgneg  14910  evth2  18987  ivth2  19354  mbfposb  19547  mbfinf  19559  mbfi1flimlem  19616  iblcnlem  19682  iblrelem  19684  itgrevallem1  19688  iblneg  19696  itgneg  19697  ibladd  19714  ditgeq1  19737  ditgeq2  19738  ditgeq3  19739  ditgneg  19746  ditgswap  19748  dvrec  19843  dvexp3  19864  dvsincos  19867  rolle  19876  dvivth  19896  dvfsumge  19908  dvfsumlem2  19913  dvfsum2  19920  ftc2ditg  19932  vieta1lem2  20230  vieta1  20231  aaliou3lem2  20262  aaliou3lem8  20264  aaliou3lem5  20266  aaliou3lem6  20267  aaliou3lem7  20268  aaliou3  20270  sinperlem  20390  efimpi  20401  ptolemy  20406  sineq0  20431  efeq1  20433  tanregt0  20443  efif1olem2  20447  lognegb  20486  logneg2  20512  advlogexp  20548  logtayl  20553  logtayl2  20555  logccv  20556  cxpmul2z  20584  cosangneg2d  20651  isosctrlem2  20665  isosctrlem3  20666  angpined  20673  dcubic1lem  20685  dcubic2  20686  mcubic  20689  cubic2  20690  dquart  20695  quart1lem  20697  quartlem1  20699  quart  20703  asinlem3a  20712  asinneg  20728  atanneg  20749  atancj  20752  atanlogaddlem  20755  atanlogsublem  20757  atantan  20765  atantayl  20779  birthdaylem3  20794  amgmlem  20830  emcllem7  20842  ftalem5  20861  basellem5  20869  basellem9  20873  lgsneg1  21106  lgseisenlem1  21135  lgseisenlem4  21138  m1lgs  21148  2sqblem  21163  dchrisum0flblem1  21204  rpvmasum2  21208  pntrsumo1  21261  pntrlog2bndlem2  21274  pntibndlem2  21287  padicfval  21312  padicval  21313  ostth3  21334  nvabs  22164  ipasslem2  22335  numdenneg  24162  xrge0iifcv  24322  xrge0iifhom  24325  xrge0iif1  24326  xrge0tmdOLD  24333  xrge0tmd  24334  logbrec  24407  lgamgulmlem2  24816  climlec3  25216  risefallfac  25342  brbtwn2  25846  colinearalglem4  25850  axsegconlem9  25866  bpoly3  26106  itg2addnclem3  26260  ibladdnc  26264  ftc1anclem5  26286  ftc1anclem6  26287  areacirclem1  26294  areacirc  26299  pellexlem6  26899  pell1234qrdich  26926  rmxm1  26999  rmym1  27000  monotoddzzfi  27007  monotoddzz  27008  oddcomabszz  27009  acongeq12d  27046  acongeq  27050  psgnunilem2  27397  itgsin0pilem1  27722  itgsinexplem1  27726  stoweidlem13  27740  stirlinglem5  27805  sigarac  27820  sigaras  27823  sigarms  27824  sigariz  27831  sigarcol  27832  sharhght  27833  sigaradd  27834  ceilingval  28590  sineq0ALT  29111
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-iota 5420  df-fv 5464  df-ov 6086  df-neg 9296
  Copyright terms: Public domain W3C validator