Theorem negeqd 11451

Description: Equality deduction for negatives. (Contributed by NM, 14-May-1999.)

Hypothesis

Ref	Expression
negeqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
negeqd	⊢ (𝜑 → -𝐴 = -𝐵)

Proof of Theorem negeqd

Step	Hyp	Ref	Expression
1		negeqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		negeq 11449	. 2 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → -𝐴 = -𝐵)

Syntax hints:   → wi 4   = wceq 1542  -cneg 11442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6493  df-fv 6549  df-ov 7409  df-neg 11444

This theorem is referenced by:  negdi  11514  mulneg2  11648  mulm1  11652  ltord2  11740  leord2  11741  eqord2  11742  divneg  11903  div2neg  11934  recgt0  12057  infrenegsup  12194  supminf  12916  mul2lt0rlt0  13073  ceilval  13800  dfceil2  13801  ceilid  13813  modcyc2  13869  monoord2  13996  expval  14026  discr  14200  reneg  15069  imneg  15077  cjcj  15084  cjneg  15091  sqeqd  15110  telfsumo2  15746  infcvgaux1i  15800  infcvgaux2i  15801  risefallfac  15965  bpoly3  15999  sinneg  16086  tanneg  16088  sincossq  16116  odd2np1  16281  oexpneg  16285  modgcd  16471  pcneg  16804  mulgval  18949  mulgneg  18967  psgnunilem2  19358  evth2  24468  ivth2  24964  mbfposb  25162  mbfinf  25174  mbfi1flimlem  25232  iblcnlem  25298  iblrelem  25300  itgrevallem1  25304  iblneg  25312  itgneg  25313  ibladd  25330  ditgeq1  25357  ditgeq2  25358  ditgeq3  25359  ditgneg  25366  ditgswap  25368  dvrec  25464  dvrecg  25482  dvmptdiv  25483  dvexp3  25487  dvsincos  25490  rolle  25499  dvivth  25519  dvfsumge  25531  dvfsumlem2  25536  dvfsum2  25543  ftc2ditg  25555  vieta1lem2  25816  vieta1  25817  aaliou3lem2  25848  aaliou3lem8  25850  aaliou3lem5  25852  aaliou3lem6  25853  aaliou3lem7  25854  aaliou3  25856  sinperlem  25982  efimpi  25993  ptolemy  25998  sineq0  26025  efeq1  26029  tanregt0  26040  efif1olem2  26044  lognegb  26090  logneg2  26115  advlogexp  26155  logtayl  26160  logtayl2  26162  logccv  26163  cxpmul2z  26191  logbrec  26277  cosangneg2d  26302  isosctrlem2  26314  isosctrlem3  26315  angpined  26325  dcubic1lem  26338  dcubic2  26339  mcubic  26342  cubic2  26343  dquart  26348  quart1lem  26350  quartlem1  26352  quart  26356  asinlem3a  26365  asinneg  26381  atanneg  26402  atancj  26405  atanlogaddlem  26408  atanlogsublem  26410  atantan  26418  atantayl  26432  birthdaylem3  26448  amgmlem  26484  emcllem7  26496  lgamgulmlem2  26524  ftalem5  26571  basellem5  26579  basellem9  26583  lgsneg1  26815  lgseisenlem1  26868  lgseisenlem4  26871  m1lgs  26881  2sqblem  26924  dchrisum0flblem1  27001  rpvmasum2  27005  pntrsumo1  27058  pntrlog2bndlem2  27071  pntibndlem2  27084  padicfval  27109  padicval  27110  ostth3  27131  brbtwn2  28153  colinearalglem4  28157  axsegconlem9  28173  ex-ceil  29691  nvabs  29913  ipasslem2  30073  numdenneg  32011  archirngz  32323  ccfldextdgrr  32735  xrge0iifcv  32903  xrge0iifhom  32906  xrge0iif1  32907  xrge0tmd  32914  xrge0tmdALT  32915  fdvneggt  33601  fdvnegge  33603  climlec3  34692  gg-dvfsumlem2  35172  dvtan  36527  itg2addnclem3  36530  ibladdnc  36534  ftc1anclem5  36554  ftc1anclem6  36555  areacirclem1  36565  areacirc  36570  dffltz  41373  3cubeslem3r  41411  pellexlem6  41558  pell1234qrdich  41585  rmxm1  41659  rmym1  41660  monotoddzzfi  41667  monotoddzz  41668  oddcomabszz  41669  acongeq12d  41704  acongeq  41708  sineq0ALT  43684  infnsuprnmpt  43941  supminfrnmpt  44142  supminfxr  44161  neglimc  44350  dvcosax  44629  itgsin0pilem1  44653  itgsinexplem1  44657  itgsincmulx  44677  stoweidlem13  44716  stirlinglem5  44781  dirkerper  44799  dirkertrigeqlem3  44803  fourierdlem39  44849  fourierdlem40  44850  fourierdlem41  44851  fourierdlem43  44853  fourierdlem49  44858  fourierdlem73  44882  fourierdlem78  44887  fourierdlem103  44912  sqwvfourb  44932  etransclem46  44983  etransclem47  44984  sigarac  45555  sigaras  45558  sigarms  45559  sigariz  45566  sigarcol  45567  sharhght  45568  sigaradd  45569  2pwp1prm  46244  oexpnegALTV  46332  oexpnegnz  46333  itschlc0yqe  47400  itsclc0yqsol  47404  itsclquadb  47416  itscnhlinecirc02plem2  47423  amgmwlem  47803