Theorem negeqd 11378

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

Syntax hints:   → wi 4   = wceq 1547  -cneg 11369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359  df-neg 11371

This theorem is referenced by:  negdi  11442  mulneg2  11578  mulm1  11582  ltord2  11670  leord2  11671  eqord2  11672  divneg  11837  div2neg  11869  recgt0  11992  infrenegsup  12130  supminf  12876  mul2lt0rlt0  13037  ceilval  13788  dfceil2  13789  ceilid  13801  modcyc2  13857  monoord2  13986  expval  14016  discr  14193  reneg  15078  imneg  15086  cjcj  15093  cjneg  15100  sqeqd  15119  telfsumo2  15757  infcvgaux1i  15813  infcvgaux2i  15814  risefallfac  15980  bpoly3  16014  sinneg  16104  tanneg  16106  sincossq  16134  odd2np1  16301  oexpneg  16305  modgcd  16492  pcneg  16836  mulgval  19038  mulgneg  19059  psgnunilem2  19461  evth2  24945  ivth2  25440  mbfposb  25638  mbfinf  25650  mbfi1flimlem  25707  iblcnlem  25774  iblrelem  25776  itgrevallem1  25780  iblneg  25788  itgneg  25789  ibladd  25806  ditgeq1  25833  ditgeq2  25834  ditgeq3  25835  ditgneg  25842  ditgswap  25844  dvrec  25940  dvrecg  25958  dvmptdiv  25959  dvexp3  25963  dvsincos  25966  rolle  25975  dvivth  25995  dvfsumge  26007  dvfsumlem2  26012  dvfsum2  26019  ftc2ditg  26031  vieta1lem2  26295  vieta1  26296  aaliou3lem2  26327  aaliou3lem8  26329  aaliou3lem5  26331  aaliou3lem6  26332  aaliou3lem7  26333  aaliou3  26335  sinperlem  26462  efimpi  26473  ptolemy  26478  sineq0  26506  efeq1  26510  tanregt0  26521  efif1olem2  26525  lognegb  26572  logneg2  26597  advlogexp  26637  logtayl  26642  logtayl2  26644  logccv  26645  cxpmul2z  26673  logbrec  26764  cosangneg2d  26789  isosctrlem2  26801  isosctrlem3  26802  angpined  26812  dcubic1lem  26825  dcubic2  26826  mcubic  26829  cubic2  26830  dquart  26835  quart1lem  26837  quartlem1  26839  quart  26843  asinlem3a  26852  asinneg  26868  atanneg  26889  atancj  26892  atanlogaddlem  26895  atanlogsublem  26897  atantan  26905  atantayl  26919  birthdaylem3  26935  amgmlem  26971  emcllem7  26983  lgamgulmlem2  27011  ftalem5  27058  basellem5  27066  basellem9  27070  lgsneg1  27303  lgseisenlem1  27356  lgseisenlem4  27359  m1lgs  27369  2sqblem  27412  dchrisum0flblem1  27489  rpvmasum2  27493  pntrsumo1  27546  pntrlog2bndlem2  27559  pntibndlem2  27572  padicfval  27597  padicval  27598  ostth3  27619  brbtwn2  28992  colinearalglem4  28996  axsegconlem9  29012  ex-ceil  30536  nvabs  30761  ipasslem2  30921  sgnval2  32827  re0cj  32835  argcj  32840  numdenneg  32907  archirngz  33270  elrgspnlem1  33323  ccfldextdgrr  33856  constrrtcc  33919  constrnegcl  33947  constrrecl  33953  cos9thpiminplylem1  33966  cos9thpiminplylem2  33967  xrge0iifcv  34118  xrge0iifhom  34121  xrge0iif1  34122  xrge0tmd  34129  xrge0tmdALT  34130  fdvneggt  34784  fdvnegge  34786  climlec3  35962  ditgeq123dv  36449  cbvditgdavw  36510  cbvditgdavw2  36526  dvtan  38037  itg2addnclem3  38040  ibladdnc  38044  ftc1anclem5  38064  ftc1anclem6  38065  areacirclem1  38075  areacirc  38080  dffltz  43084  3cubeslem3r  43136  pellexlem6  43279  pell1234qrdich  43306  rmxm1  43379  rmym1  43380  monotoddzzfi  43387  monotoddzz  43388  oddcomabszz  43389  acongeq12d  43424  acongeq  43428  sineq0ALT  45380  infnsuprnmpt  45694  supminfrnmpt  45888  supminfxr  45907  neglimc  46090  dvcosax  46369  itgsin0pilem1  46393  itgsinexplem1  46397  itgsincmulx  46417  stoweidlem13  46456  stirlinglem5  46521  dirkerper  46539  dirkertrigeqlem3  46543  fourierdlem39  46589  fourierdlem40  46590  fourierdlem41  46591  fourierdlem43  46593  fourierdlem49  46598  fourierdlem73  46622  fourierdlem78  46627  fourierdlem103  46652  sqwvfourb  46672  etransclem46  46723  etransclem47  46724  sigarac  47295  sigaras  47298  sigarms  47299  sigariz  47306  sigarcol  47307  sharhght  47308  sigaradd  47309  nthrucw  47331  ceildivmod  47808  difmodm1lt  47828  2pwp1prm  48067  oexpnegALTV  48168  oexpnegnz  48169  itschlc0yqe  49251  itsclc0yqsol  49255  itsclquadb  49267  itscnhlinecirc02plem2  49274  amgmwlem  50292