Theorem negeqd 11354

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

Syntax hints:   → wi 4   = wceq 1541  -cneg 11345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349  df-neg 11347

This theorem is referenced by:  negdi  11418  mulneg2  11554  mulm1  11558  ltord2  11646  leord2  11647  eqord2  11648  divneg  11813  div2neg  11844  recgt0  11967  infrenegsup  12105  supminf  12833  mul2lt0rlt0  12994  ceilval  13742  dfceil2  13743  ceilid  13755  modcyc2  13811  monoord2  13940  expval  13970  discr  14147  reneg  15032  imneg  15040  cjcj  15047  cjneg  15054  sqeqd  15073  telfsumo2  15710  infcvgaux1i  15764  infcvgaux2i  15765  risefallfac  15931  bpoly3  15965  sinneg  16055  tanneg  16057  sincossq  16085  odd2np1  16252  oexpneg  16256  modgcd  16443  pcneg  16786  mulgval  18984  mulgneg  19005  psgnunilem2  19407  evth2  24886  ivth2  25383  mbfposb  25581  mbfinf  25593  mbfi1flimlem  25650  iblcnlem  25717  iblrelem  25719  itgrevallem1  25723  iblneg  25731  itgneg  25732  ibladd  25749  ditgeq1  25776  ditgeq2  25777  ditgeq3  25778  ditgneg  25785  ditgswap  25787  dvrec  25886  dvrecg  25904  dvmptdiv  25905  dvexp3  25909  dvsincos  25912  rolle  25921  dvivth  25942  dvfsumge  25955  dvfsumlem2  25960  dvfsumlem2OLD  25961  dvfsum2  25968  ftc2ditg  25980  vieta1lem2  26246  vieta1  26247  aaliou3lem2  26278  aaliou3lem8  26280  aaliou3lem5  26282  aaliou3lem6  26283  aaliou3lem7  26284  aaliou3  26286  sinperlem  26416  efimpi  26427  ptolemy  26432  sineq0  26460  efeq1  26464  tanregt0  26475  efif1olem2  26479  lognegb  26526  logneg2  26551  advlogexp  26591  logtayl  26596  logtayl2  26598  logccv  26599  cxpmul2z  26627  logbrec  26719  cosangneg2d  26744  isosctrlem2  26756  isosctrlem3  26757  angpined  26767  dcubic1lem  26780  dcubic2  26781  mcubic  26784  cubic2  26785  dquart  26790  quart1lem  26792  quartlem1  26794  quart  26798  asinlem3a  26807  asinneg  26823  atanneg  26844  atancj  26847  atanlogaddlem  26850  atanlogsublem  26852  atantan  26860  atantayl  26874  birthdaylem3  26890  amgmlem  26927  emcllem7  26939  lgamgulmlem2  26967  ftalem5  27014  basellem5  27022  basellem9  27026  lgsneg1  27260  lgseisenlem1  27313  lgseisenlem4  27316  m1lgs  27326  2sqblem  27369  dchrisum0flblem1  27446  rpvmasum2  27450  pntrsumo1  27503  pntrlog2bndlem2  27516  pntibndlem2  27529  padicfval  27554  padicval  27555  ostth3  27576  brbtwn2  28883  colinearalglem4  28887  axsegconlem9  28903  ex-ceil  30428  nvabs  30652  ipasslem2  30812  sgnval2  32718  re0cj  32727  argcj  32732  numdenneg  32797  archirngz  33158  elrgspnlem1  33209  ccfldextdgrr  33685  constrrtcc  33748  constrnegcl  33776  constrrecl  33782  cos9thpiminplylem1  33795  cos9thpiminplylem2  33796  xrge0iifcv  33947  xrge0iifhom  33950  xrge0iif1  33951  xrge0tmd  33958  xrge0tmdALT  33959  fdvneggt  34613  fdvnegge  34615  climlec3  35778  ditgeq123dv  36265  cbvditgdavw  36326  cbvditgdavw2  36342  dvtan  37720  itg2addnclem3  37723  ibladdnc  37727  ftc1anclem5  37747  ftc1anclem6  37748  areacirclem1  37758  areacirc  37763  dffltz  42737  3cubeslem3r  42790  pellexlem6  42937  pell1234qrdich  42964  rmxm1  43037  rmym1  43038  monotoddzzfi  43045  monotoddzz  43046  oddcomabszz  43047  acongeq12d  43082  acongeq  43086  sineq0ALT  45039  infnsuprnmpt  45357  supminfrnmpt  45553  supminfxr  45572  neglimc  45755  dvcosax  46034  itgsin0pilem1  46058  itgsinexplem1  46062  itgsincmulx  46082  stoweidlem13  46121  stirlinglem5  46186  dirkerper  46204  dirkertrigeqlem3  46208  fourierdlem39  46254  fourierdlem40  46255  fourierdlem41  46256  fourierdlem43  46258  fourierdlem49  46263  fourierdlem73  46287  fourierdlem78  46292  fourierdlem103  46317  sqwvfourb  46337  etransclem46  46388  etransclem47  46389  sigarac  46960  sigaras  46963  sigarms  46964  sigariz  46971  sigarcol  46972  sharhght  46973  sigaradd  46974  nthrucw  46994  ceildivmod  47449  difmodm1lt  47469  2pwp1prm  47699  oexpnegALTV  47787  oexpnegnz  47788  itschlc0yqe  48871  itsclc0yqsol  48875  itsclquadb  48887  itscnhlinecirc02plem2  48894  amgmwlem  49913