Theorem negeqd 11500

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

Syntax hints:   → wi 4   = wceq 1537  -cneg 11491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434  df-neg 11493

This theorem is referenced by:  negdi  11564  mulneg2  11698  mulm1  11702  ltord2  11790  leord2  11791  eqord2  11792  divneg  11957  div2neg  11988  recgt0  12111  infrenegsup  12249  supminf  12975  mul2lt0rlt0  13135  ceilval  13875  dfceil2  13876  ceilid  13888  modcyc2  13944  monoord2  14071  expval  14101  discr  14276  reneg  15161  imneg  15169  cjcj  15176  cjneg  15183  sqeqd  15202  telfsumo2  15836  infcvgaux1i  15890  infcvgaux2i  15891  risefallfac  16057  bpoly3  16091  sinneg  16179  tanneg  16181  sincossq  16209  odd2np1  16375  oexpneg  16379  modgcd  16566  pcneg  16908  mulgval  19102  mulgneg  19123  psgnunilem2  19528  evth2  25006  ivth2  25504  mbfposb  25702  mbfinf  25714  mbfi1flimlem  25772  iblcnlem  25839  iblrelem  25841  itgrevallem1  25845  iblneg  25853  itgneg  25854  ibladd  25871  ditgeq1  25898  ditgeq2  25899  ditgeq3  25900  ditgneg  25907  ditgswap  25909  dvrec  26008  dvrecg  26026  dvmptdiv  26027  dvexp3  26031  dvsincos  26034  rolle  26043  dvivth  26064  dvfsumge  26077  dvfsumlem2  26082  dvfsumlem2OLD  26083  dvfsum2  26090  ftc2ditg  26102  vieta1lem2  26368  vieta1  26369  aaliou3lem2  26400  aaliou3lem8  26402  aaliou3lem5  26404  aaliou3lem6  26405  aaliou3lem7  26406  aaliou3  26408  sinperlem  26537  efimpi  26548  ptolemy  26553  sineq0  26581  efeq1  26585  tanregt0  26596  efif1olem2  26600  lognegb  26647  logneg2  26672  advlogexp  26712  logtayl  26717  logtayl2  26719  logccv  26720  cxpmul2z  26748  logbrec  26840  cosangneg2d  26865  isosctrlem2  26877  isosctrlem3  26878  angpined  26888  dcubic1lem  26901  dcubic2  26902  mcubic  26905  cubic2  26906  dquart  26911  quart1lem  26913  quartlem1  26915  quart  26919  asinlem3a  26928  asinneg  26944  atanneg  26965  atancj  26968  atanlogaddlem  26971  atanlogsublem  26973  atantan  26981  atantayl  26995  birthdaylem3  27011  amgmlem  27048  emcllem7  27060  lgamgulmlem2  27088  ftalem5  27135  basellem5  27143  basellem9  27147  lgsneg1  27381  lgseisenlem1  27434  lgseisenlem4  27437  m1lgs  27447  2sqblem  27490  dchrisum0flblem1  27567  rpvmasum2  27571  pntrsumo1  27624  pntrlog2bndlem2  27637  pntibndlem2  27650  padicfval  27675  padicval  27676  ostth3  27697  brbtwn2  28935  colinearalglem4  28939  axsegconlem9  28955  ex-ceil  30477  nvabs  30701  ipasslem2  30861  re0cj  32760  numdenneg  32821  archirngz  33179  elrgspnlem1  33232  ccfldextdgrr  33697  constrrtcc  33741  xrge0iifcv  33895  xrge0iifhom  33898  xrge0iif1  33899  xrge0tmd  33906  xrge0tmdALT  33907  fdvneggt  34594  fdvnegge  34596  climlec3  35714  ditgeq123dv  36204  cbvditgdavw  36265  cbvditgdavw2  36281  dvtan  37657  itg2addnclem3  37660  ibladdnc  37664  ftc1anclem5  37684  ftc1anclem6  37685  areacirclem1  37695  areacirc  37700  dffltz  42621  3cubeslem3r  42675  pellexlem6  42822  pell1234qrdich  42849  rmxm1  42923  rmym1  42924  monotoddzzfi  42931  monotoddzz  42932  oddcomabszz  42933  acongeq12d  42968  acongeq  42972  sineq0ALT  44935  infnsuprnmpt  45195  supminfrnmpt  45395  supminfxr  45414  neglimc  45603  dvcosax  45882  itgsin0pilem1  45906  itgsinexplem1  45910  itgsincmulx  45930  stoweidlem13  45969  stirlinglem5  46034  dirkerper  46052  dirkertrigeqlem3  46056  fourierdlem39  46102  fourierdlem40  46103  fourierdlem41  46104  fourierdlem43  46106  fourierdlem49  46111  fourierdlem73  46135  fourierdlem78  46140  fourierdlem103  46165  sqwvfourb  46185  etransclem46  46236  etransclem47  46237  sigarac  46808  sigaras  46811  sigarms  46812  sigariz  46819  sigarcol  46820  sharhght  46821  sigaradd  46822  ceildivmod  47279  2pwp1prm  47514  oexpnegALTV  47602  oexpnegnz  47603  itschlc0yqe  48610  itsclc0yqsol  48614  itsclquadb  48626  itscnhlinecirc02plem2  48633  amgmwlem  49033