Theorem negeqd 11374

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

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

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-neg 11367

This theorem is referenced by:  negdi  11438  mulneg2  11574  mulm1  11578  ltord2  11666  leord2  11667  eqord2  11668  divneg  11833  div2neg  11864  recgt0  11987  infrenegsup  12125  supminf  12848  mul2lt0rlt0  13009  ceilval  13758  dfceil2  13759  ceilid  13771  modcyc2  13827  monoord2  13956  expval  13986  discr  14163  reneg  15048  imneg  15056  cjcj  15063  cjneg  15070  sqeqd  15089  telfsumo2  15726  infcvgaux1i  15780  infcvgaux2i  15781  risefallfac  15947  bpoly3  15981  sinneg  16071  tanneg  16073  sincossq  16101  odd2np1  16268  oexpneg  16272  modgcd  16459  pcneg  16802  mulgval  19001  mulgneg  19022  psgnunilem2  19424  evth2  24915  ivth2  25412  mbfposb  25610  mbfinf  25622  mbfi1flimlem  25679  iblcnlem  25746  iblrelem  25748  itgrevallem1  25752  iblneg  25760  itgneg  25761  ibladd  25778  ditgeq1  25805  ditgeq2  25806  ditgeq3  25807  ditgneg  25814  ditgswap  25816  dvrec  25915  dvrecg  25933  dvmptdiv  25934  dvexp3  25938  dvsincos  25941  rolle  25950  dvivth  25971  dvfsumge  25984  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsum2  25997  ftc2ditg  26009  vieta1lem2  26275  vieta1  26276  aaliou3lem2  26307  aaliou3lem8  26309  aaliou3lem5  26311  aaliou3lem6  26312  aaliou3lem7  26313  aaliou3  26315  sinperlem  26445  efimpi  26456  ptolemy  26461  sineq0  26489  efeq1  26493  tanregt0  26504  efif1olem2  26508  lognegb  26555  logneg2  26580  advlogexp  26620  logtayl  26625  logtayl2  26627  logccv  26628  cxpmul2z  26656  logbrec  26748  cosangneg2d  26773  isosctrlem2  26785  isosctrlem3  26786  angpined  26796  dcubic1lem  26809  dcubic2  26810  mcubic  26813  cubic2  26814  dquart  26819  quart1lem  26821  quartlem1  26823  quart  26827  asinlem3a  26836  asinneg  26852  atanneg  26873  atancj  26876  atanlogaddlem  26879  atanlogsublem  26881  atantan  26889  atantayl  26903  birthdaylem3  26919  amgmlem  26956  emcllem7  26968  lgamgulmlem2  26996  ftalem5  27043  basellem5  27051  basellem9  27055  lgsneg1  27289  lgseisenlem1  27342  lgseisenlem4  27345  m1lgs  27355  2sqblem  27398  dchrisum0flblem1  27475  rpvmasum2  27479  pntrsumo1  27532  pntrlog2bndlem2  27545  pntibndlem2  27558  padicfval  27583  padicval  27584  ostth3  27605  brbtwn2  28978  colinearalglem4  28982  axsegconlem9  28998  ex-ceil  30523  nvabs  30747  ipasslem2  30907  sgnval2  32814  re0cj  32823  argcj  32828  numdenneg  32895  archirngz  33271  elrgspnlem1  33324  ccfldextdgrr  33829  constrrtcc  33892  constrnegcl  33920  constrrecl  33926  cos9thpiminplylem1  33939  cos9thpiminplylem2  33940  xrge0iifcv  34091  xrge0iifhom  34094  xrge0iif1  34095  xrge0tmd  34102  xrge0tmdALT  34103  fdvneggt  34757  fdvnegge  34759  climlec3  35928  ditgeq123dv  36415  cbvditgdavw  36476  cbvditgdavw2  36492  dvtan  37871  itg2addnclem3  37874  ibladdnc  37878  ftc1anclem5  37898  ftc1anclem6  37899  areacirclem1  37909  areacirc  37914  dffltz  42887  3cubeslem3r  42939  pellexlem6  43086  pell1234qrdich  43113  rmxm1  43186  rmym1  43187  monotoddzzfi  43194  monotoddzz  43195  oddcomabszz  43196  acongeq12d  43231  acongeq  43235  sineq0ALT  45187  infnsuprnmpt  45504  supminfrnmpt  45699  supminfxr  45718  neglimc  45901  dvcosax  46180  itgsin0pilem1  46204  itgsinexplem1  46208  itgsincmulx  46228  stoweidlem13  46267  stirlinglem5  46332  dirkerper  46350  dirkertrigeqlem3  46354  fourierdlem39  46400  fourierdlem40  46401  fourierdlem41  46402  fourierdlem43  46404  fourierdlem49  46409  fourierdlem73  46433  fourierdlem78  46438  fourierdlem103  46463  sqwvfourb  46483  etransclem46  46534  etransclem47  46535  sigarac  47106  sigaras  47109  sigarms  47110  sigariz  47117  sigarcol  47118  sharhght  47119  sigaradd  47120  nthrucw  47140  ceildivmod  47595  difmodm1lt  47615  2pwp1prm  47845  oexpnegALTV  47933  oexpnegnz  47934  itschlc0yqe  49016  itsclc0yqsol  49020  itsclquadb  49032  itscnhlinecirc02plem2  49039  amgmwlem  50057