Theorem negeqd 10154

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

Syntax hints:   → wi 4   = wceq 1475  -cneg 10146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-neg 10148

This theorem is referenced by:  negdi  10217  mulneg2  10346  mulm1  10350  ltord2  10436  leord2  10437  eqord2  10438  divneg  10598  div2neg  10627  recgt0  10746  infrenegsup  10883  supminf  11651  mul2lt0rlt0  11808  ceilval  12501  dfceil2  12502  ceilid  12512  modcyc2  12568  monoord2  12694  expval  12724  discr  12863  reneg  13713  imneg  13721  cjcj  13728  cjneg  13735  sqeqd  13754  telfsumo2  14376  infcvgaux1i  14428  infcvgaux2i  14429  risefallfac  14594  bpoly3  14628  sinneg  14715  tanneg  14717  sincossq  14745  odd2np1  14903  oexpneg  14907  modgcd  15091  pcneg  15416  mulgval  17366  mulgneg  17383  psgnunilem2  17738  evth2  22567  ivth2  23031  mbfposb  23226  mbfinf  23238  mbfi1flimlem  23295  iblcnlem  23361  iblrelem  23363  itgrevallem1  23367  iblneg  23375  itgneg  23376  ibladd  23393  ditgeq1  23418  ditgeq2  23419  ditgeq3  23420  ditgneg  23427  ditgswap  23429  dvrec  23524  dvexp3  23545  dvsincos  23548  rolle  23557  dvivth  23577  dvfsumge  23589  dvfsumlem2  23594  dvfsum2  23601  ftc2ditg  23613  vieta1lem2  23870  vieta1  23871  aaliou3lem2  23902  aaliou3lem8  23904  aaliou3lem5  23906  aaliou3lem6  23907  aaliou3lem7  23908  aaliou3  23910  sinperlem  24036  efimpi  24047  ptolemy  24052  sineq0  24077  efeq1  24079  tanregt0  24089  efif1olem2  24093  lognegb  24140  logneg2  24165  advlogexp  24201  logtayl  24206  logtayl2  24208  logccv  24209  cxpmul2z  24237  logbrec  24320  cosangneg2d  24337  isosctrlem2  24349  isosctrlem3  24350  angpined  24357  dcubic1lem  24370  dcubic2  24371  mcubic  24374  cubic2  24375  dquart  24380  quart1lem  24382  quartlem1  24384  quart  24388  asinlem3a  24397  asinneg  24413  atanneg  24434  atancj  24437  atanlogaddlem  24440  atanlogsublem  24442  atantan  24450  atantayl  24464  birthdaylem3  24480  amgmlem  24516  emcllem7  24528  lgamgulmlem2  24556  ftalem5  24603  basellem5  24611  basellem9  24615  lgsneg1  24847  lgseisenlem1  24900  lgseisenlem4  24903  m1lgs  24913  2sqblem  24956  dchrisum0flblem1  24997  rpvmasum2  25001  pntrsumo1  25054  pntrlog2bndlem2  25067  pntibndlem2  25080  padicfval  25105  padicval  25106  ostth3  25127  brbtwn2  25585  colinearalglem4  25589  axsegconlem9  25605  ex-ceil  26697  nvabs  26911  ipasslem2  27071  numdenneg  28950  archirngz  29074  xrge0iifcv  29308  xrge0iifhom  29311  xrge0iif1  29312  xrge0tmdOLD  29319  xrge0tmd  29320  climlec3  30872  dvtan  32630  itg2addnclem3  32633  ibladdnc  32637  ftc1anclem5  32659  ftc1anclem6  32660  areacirclem1  32670  areacirc  32675  pellexlem6  36416  pell1234qrdich  36443  rmxm1  36517  rmym1  36518  monotoddzzfi  36525  monotoddzz  36526  oddcomabszz  36527  acongeq12d  36564  acongeq  36568  sineq0ALT  38195  neglimc  38714  dvrecg  38800  dvmptdiv  38807  dvcosax  38816  itgsin0pilem1  38841  itgsinexplem1  38845  itgsincmulx  38866  stoweidlem13  38906  stirlinglem5  38971  dirkerper  38989  dirkertrigeqlem3  38993  fourierdlem39  39039  fourierdlem40  39040  fourierdlem41  39041  fourierdlem43  39043  fourierdlem49  39048  fourierdlem73  39072  fourierdlem78  39077  fourierdlem103  39102  sqwvfourb  39122  etransclem46  39173  etransclem47  39174  sigarac  39690  sigaras  39693  sigarms  39694  sigariz  39701  sigarcol  39702  sharhght  39703  sigaradd  39704  2pwp1prm  40041  oexpnegALTV  40126  oexpnegnz  40127  amgmwlem  42357