Theorem negeqd 11357

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

Syntax hints:   → wi 4   = wceq 1540  -cneg 11348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-neg 11350

This theorem is referenced by:  negdi  11421  mulneg2  11557  mulm1  11561  ltord2  11649  leord2  11650  eqord2  11651  divneg  11816  div2neg  11847  recgt0  11970  infrenegsup  12108  supminf  12836  mul2lt0rlt0  12997  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  18950  mulgneg  18971  psgnunilem2  19374  evth2  24857  ivth2  25354  mbfposb  25552  mbfinf  25564  mbfi1flimlem  25621  iblcnlem  25688  iblrelem  25690  itgrevallem1  25694  iblneg  25702  itgneg  25703  ibladd  25720  ditgeq1  25747  ditgeq2  25748  ditgeq3  25749  ditgneg  25756  ditgswap  25758  dvrec  25857  dvrecg  25875  dvmptdiv  25876  dvexp3  25880  dvsincos  25883  rolle  25892  dvivth  25913  dvfsumge  25926  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsum2  25939  ftc2ditg  25951  vieta1lem2  26217  vieta1  26218  aaliou3lem2  26249  aaliou3lem8  26251  aaliou3lem5  26253  aaliou3lem6  26254  aaliou3lem7  26255  aaliou3  26257  sinperlem  26387  efimpi  26398  ptolemy  26403  sineq0  26431  efeq1  26435  tanregt0  26446  efif1olem2  26450  lognegb  26497  logneg2  26522  advlogexp  26562  logtayl  26567  logtayl2  26569  logccv  26570  cxpmul2z  26598  logbrec  26690  cosangneg2d  26715  isosctrlem2  26727  isosctrlem3  26728  angpined  26738  dcubic1lem  26751  dcubic2  26752  mcubic  26755  cubic2  26756  dquart  26761  quart1lem  26763  quartlem1  26765  quart  26769  asinlem3a  26778  asinneg  26794  atanneg  26815  atancj  26818  atanlogaddlem  26821  atanlogsublem  26823  atantan  26831  atantayl  26845  birthdaylem3  26861  amgmlem  26898  emcllem7  26910  lgamgulmlem2  26938  ftalem5  26985  basellem5  26993  basellem9  26997  lgsneg1  27231  lgseisenlem1  27284  lgseisenlem4  27287  m1lgs  27297  2sqblem  27340  dchrisum0flblem1  27417  rpvmasum2  27421  pntrsumo1  27474  pntrlog2bndlem2  27487  pntibndlem2  27500  padicfval  27525  padicval  27526  ostth3  27547  brbtwn2  28850  colinearalglem4  28854  axsegconlem9  28870  ex-ceil  30392  nvabs  30616  ipasslem2  30776  sgnval2  32679  re0cj  32688  argcj  32693  numdenneg  32760  archirngz  33132  elrgspnlem1  33183  ccfldextdgrr  33645  constrrtcc  33708  constrnegcl  33736  constrrecl  33742  cos9thpiminplylem1  33755  cos9thpiminplylem2  33756  xrge0iifcv  33907  xrge0iifhom  33910  xrge0iif1  33911  xrge0tmd  33918  xrge0tmdALT  33919  fdvneggt  34574  fdvnegge  34576  climlec3  35717  ditgeq123dv  36205  cbvditgdavw  36266  cbvditgdavw2  36282  dvtan  37660  itg2addnclem3  37663  ibladdnc  37667  ftc1anclem5  37687  ftc1anclem6  37688  areacirclem1  37698  areacirc  37703  dffltz  42617  3cubeslem3r  42670  pellexlem6  42817  pell1234qrdich  42844  rmxm1  42917  rmym1  42918  monotoddzzfi  42925  monotoddzz  42926  oddcomabszz  42927  acongeq12d  42962  acongeq  42966  sineq0ALT  44920  infnsuprnmpt  45238  supminfrnmpt  45434  supminfxr  45453  neglimc  45638  dvcosax  45917  itgsin0pilem1  45941  itgsinexplem1  45945  itgsincmulx  45965  stoweidlem13  46004  stirlinglem5  46069  dirkerper  46087  dirkertrigeqlem3  46091  fourierdlem39  46137  fourierdlem40  46138  fourierdlem41  46139  fourierdlem43  46141  fourierdlem49  46146  fourierdlem73  46170  fourierdlem78  46175  fourierdlem103  46200  sqwvfourb  46220  etransclem46  46271  etransclem47  46272  sigarac  46843  sigaras  46846  sigarms  46847  sigariz  46854  sigarcol  46855  sharhght  46856  sigaradd  46857  ceildivmod  47333  difmodm1lt  47353  2pwp1prm  47583  oexpnegALTV  47671  oexpnegnz  47672  itschlc0yqe  48755  itsclc0yqsol  48759  itsclquadb  48771  itscnhlinecirc02plem2  48778  amgmwlem  49797