Theorem negeqd 11145

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 11143	. 2 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → -𝐴 = -𝐵)

Syntax hints:   → wi 4   = wceq 1539  -cneg 11136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-neg 11138

This theorem is referenced by:  negdi  11208  mulneg2  11342  mulm1  11346  ltord2  11434  leord2  11435  eqord2  11436  divneg  11597  div2neg  11628  recgt0  11751  infrenegsup  11888  supminf  12604  mul2lt0rlt0  12761  ceilval  13486  dfceil2  13487  ceilid  13499  modcyc2  13555  monoord2  13682  expval  13712  discr  13883  reneg  14764  imneg  14772  cjcj  14779  cjneg  14786  sqeqd  14805  telfsumo2  15443  infcvgaux1i  15497  infcvgaux2i  15498  risefallfac  15662  bpoly3  15696  sinneg  15783  tanneg  15785  sincossq  15813  odd2np1  15978  oexpneg  15982  modgcd  16168  pcneg  16503  mulgval  18619  mulgneg  18637  psgnunilem2  19018  evth2  24029  ivth2  24524  mbfposb  24722  mbfinf  24734  mbfi1flimlem  24792  iblcnlem  24858  iblrelem  24860  itgrevallem1  24864  iblneg  24872  itgneg  24873  ibladd  24890  ditgeq1  24917  ditgeq2  24918  ditgeq3  24919  ditgneg  24926  ditgswap  24928  dvrec  25024  dvrecg  25042  dvmptdiv  25043  dvexp3  25047  dvsincos  25050  rolle  25059  dvivth  25079  dvfsumge  25091  dvfsumlem2  25096  dvfsum2  25103  ftc2ditg  25115  vieta1lem2  25376  vieta1  25377  aaliou3lem2  25408  aaliou3lem8  25410  aaliou3lem5  25412  aaliou3lem6  25413  aaliou3lem7  25414  aaliou3  25416  sinperlem  25542  efimpi  25553  ptolemy  25558  sineq0  25585  efeq1  25589  tanregt0  25600  efif1olem2  25604  lognegb  25650  logneg2  25675  advlogexp  25715  logtayl  25720  logtayl2  25722  logccv  25723  cxpmul2z  25751  logbrec  25837  cosangneg2d  25862  isosctrlem2  25874  isosctrlem3  25875  angpined  25885  dcubic1lem  25898  dcubic2  25899  mcubic  25902  cubic2  25903  dquart  25908  quart1lem  25910  quartlem1  25912  quart  25916  asinlem3a  25925  asinneg  25941  atanneg  25962  atancj  25965  atanlogaddlem  25968  atanlogsublem  25970  atantan  25978  atantayl  25992  birthdaylem3  26008  amgmlem  26044  emcllem7  26056  lgamgulmlem2  26084  ftalem5  26131  basellem5  26139  basellem9  26143  lgsneg1  26375  lgseisenlem1  26428  lgseisenlem4  26431  m1lgs  26441  2sqblem  26484  dchrisum0flblem1  26561  rpvmasum2  26565  pntrsumo1  26618  pntrlog2bndlem2  26631  pntibndlem2  26644  padicfval  26669  padicval  26670  ostth3  26691  brbtwn2  27176  colinearalglem4  27180  axsegconlem9  27196  ex-ceil  28713  nvabs  28935  ipasslem2  29095  numdenneg  31033  archirngz  31345  ccfldextdgrr  31644  xrge0iifcv  31786  xrge0iifhom  31789  xrge0iif1  31790  xrge0tmd  31797  xrge0tmdALT  31798  fdvneggt  32480  fdvnegge  32482  climlec3  33605  dvtan  35754  itg2addnclem3  35757  ibladdnc  35761  ftc1anclem5  35781  ftc1anclem6  35782  areacirclem1  35792  areacirc  35797  dffltz  40387  3cubeslem3r  40425  pellexlem6  40572  pell1234qrdich  40599  rmxm1  40672  rmym1  40673  monotoddzzfi  40680  monotoddzz  40681  oddcomabszz  40682  acongeq12d  40717  acongeq  40721  sineq0ALT  42446  infnsuprnmpt  42685  supminfrnmpt  42875  supminfxr  42894  neglimc  43078  dvcosax  43357  itgsin0pilem1  43381  itgsinexplem1  43385  itgsincmulx  43405  stoweidlem13  43444  stirlinglem5  43509  dirkerper  43527  dirkertrigeqlem3  43531  fourierdlem39  43577  fourierdlem40  43578  fourierdlem41  43579  fourierdlem43  43581  fourierdlem49  43586  fourierdlem73  43610  fourierdlem78  43615  fourierdlem103  43640  sqwvfourb  43660  etransclem46  43711  etransclem47  43712  sigarac  44255  sigaras  44258  sigarms  44259  sigariz  44266  sigarcol  44267  sharhght  44268  sigaradd  44269  2pwp1prm  44929  oexpnegALTV  45017  oexpnegnz  45018  itschlc0yqe  45994  itsclc0yqsol  45998  itsclquadb  46010  itscnhlinecirc02plem2  46017  amgmwlem  46392