Theorem negeqd 11478

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  -cneg 11469

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417  df-neg 11471

This theorem is used by:  negdi  11542  mulneg2  11678  mulm1  11682  ltord2  11770  leord2  11771  eqord2  11772  divneg  11933  div2neg  11965  recgt0  12088  infrenegsup  12225  supminf  12987  mul2lt0rlt0  13149  ceilval  13902  dfceil2  13903  ceilid  13915  modcyc2  13971  monoord2  14100  expval  14130  discr  14307  reneg  15215  imneg  15223  cjcj  15230  cjneg  15237  sqeqd  15256  telfsumo2  15893  infcvgaux1i  15949  infcvgaux2i  15950  risefallfac  16114  bpoly3  16147  sinneg  16237  tanneg  16239  sincossq  16267  odd2np1  16434  oexpneg  16438  modgcd  16625  pcneg  16969  mulgval  19197  mulgneg  19218  psgnunilem2  19625  evth2  25191  ivth2  25686  mbfposb  25884  mbfinf  25896  mbfi1flimlem  25953  iblcnlem  26019  iblrelem  26021  itgrevallem1  26025  iblneg  26033  itgneg  26034  ibladd  26051  ditgeq1  26078  ditgeq2  26079  ditgeq3  26080  ditgneg  26087  ditgswap  26089  dvrec  26185  dvrecg  26203  dvmptdiv  26204  dvexp3  26208  dvsincos  26211  rolle  26220  dvivth  26240  dvfsumge  26252  dvfsumlem2  26257  dvfsum2  26264  ftc2ditg  26276  vieta1lem2  26546  vieta1  26547  aaliou3lem2  26582  aaliou3lem8  26584  aaliou3lem5  26586  aaliou3lem6  26587  aaliou3lem7  26588  aaliou3  26590  aaliou3r  26591  sinperlem  26721  efimpi  26732  ptolemy  26737  sineq0  26764  efeq1  26768  tanregt0  26779  efif1olem2  26783  lognegb  26830  logneg2  26855  advlogexp  26895  logtayl  26900  logtayl2  26902  logccv  26903  cxpmul2z  26931  logbrec  27022  cosangneg2d  27047  isosctrlem2  27059  isosctrlem3  27060  angpined  27070  dcubic1lem  27083  dcubic2  27084  mcubic  27087  cubic2  27088  dquart  27093  quart1lem  27095  quartlem1  27097  quart  27101  asinlem3a  27110  asinneg  27126  atanneg  27147  atancj  27150  atanlogaddlem  27153  atanlogsublem  27155  atantan  27163  atantayl  27177  birthdaylem3  27193  amgmlem  27229  emcllem7  27241  lgamgulmlem2  27269  ftalem5  27316  basellem5  27324  basellem9  27328  lgsneg1  27561  lgseisenlem1  27614  lgseisenlem4  27617  m1lgs  27627  2sqblem  27670  dchrisum0flblem1  27747  rpvmasum2  27751  pntrsumo1  27804  pntrlog2bndlem2  27817  pntibndlem2  27830  padicfval  27855  padicval  27856  ostth3  27877  brbtwn2  29365  colinearalglem4  29369  axsegconlem9  29385  ex-ceil  30931  nvabs  31156  ipasslem2  31316  sgnval2  33209  re0cj  33217  argcj  33222  numdenneg  33288  archirngz  33632  elrgspnlem1  33685  ccfldextdgrr  34185  constrrtcc  34248  constrnegcl  34276  constrrecl  34282  cos9thpiminplylem1  34295  cos9thpiminplylem2  34296  xrge0iifcv  34447  xrge0iifhom  34450  xrge0iif1  34451  xrge0tmd  34458  xrge0tmdALT  34459  fdvneggt  35111  fdvnegge  35113  climlec3  36316  ditgeq123dv  36844  cbvditgdavw  36905  cbvditgdavw2  36921  dvtan  38422  itg2addnclem3  38425  ibladdnc  38429  ftc1anclem5  38449  ftc1anclem6  38450  areacirclem1  38460  areacirc  38465  25or6to4  43075  dffltz  43483  3cubeslem3r  43535  pellexlem6  43678  pell1234qrdich  43705  rmxm1  43778  rmym1  43779  monotoddzzfi  43786  monotoddzz  43787  oddcomabszz  43788  acongeq12d  43823  acongeq  43827  sineq0ALT  45762  infnsuprnmpt  46082  supminfrnmpt  46276  supminfxr  46295  neglimc  46478  dvcosax  46757  itgsin0pilem1  46781  itgsinexplem1  46785  itgsincmulx  46805  stoweidlem13  46844  stirlinglem5  46909  dirkerper  46927  dirkertrigeqlem3  46931  fourierdlem39  46977  fourierdlem40  46978  fourierdlem41  46979  fourierdlem43  46981  fourierdlem49  46986  fourierdlem73  47010  fourierdlem78  47015  fourierdlem103  47040  sqwvfourb  47060  etransclem46  47111  etransclem47  47112  sigarac  47683  sigaras  47686  sigarms  47687  sigariz  47694  sigarcol  47695  sharhght  47696  sigaradd  47697  ceildivmod  48236  difmodm1lt  48256  2pwp1prm  48495  oexpnegALTV  48596  oexpnegnz  48597  itschlc0yqe  49693  itsclc0yqsol  49697  itsclquadb  49709  itscnhlinecirc02plem2  49716  dvsec  50692  dvcsc  50693  dvcot  50694  crosspaltd  50802  amgmwlem  50823