Theorem negeqd 11391

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

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

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-neg 11384

This theorem is referenced by:  negdi  11455  mulneg2  11591  mulm1  11595  ltord2  11683  leord2  11684  eqord2  11685  divneg  11850  div2neg  11881  recgt0  12004  infrenegsup  12142  supminf  12870  mul2lt0rlt0  13031  ceilval  13776  dfceil2  13777  ceilid  13789  modcyc2  13845  monoord2  13974  expval  14004  discr  14181  reneg  15067  imneg  15075  cjcj  15082  cjneg  15089  sqeqd  15108  telfsumo2  15745  infcvgaux1i  15799  infcvgaux2i  15800  risefallfac  15966  bpoly3  16000  sinneg  16090  tanneg  16092  sincossq  16120  odd2np1  16287  oexpneg  16291  modgcd  16478  pcneg  16821  mulgval  18985  mulgneg  19006  psgnunilem2  19409  evth2  24892  ivth2  25389  mbfposb  25587  mbfinf  25599  mbfi1flimlem  25656  iblcnlem  25723  iblrelem  25725  itgrevallem1  25729  iblneg  25737  itgneg  25738  ibladd  25755  ditgeq1  25782  ditgeq2  25783  ditgeq3  25784  ditgneg  25791  ditgswap  25793  dvrec  25892  dvrecg  25910  dvmptdiv  25911  dvexp3  25915  dvsincos  25918  rolle  25927  dvivth  25948  dvfsumge  25961  dvfsumlem2  25966  dvfsumlem2OLD  25967  dvfsum2  25974  ftc2ditg  25986  vieta1lem2  26252  vieta1  26253  aaliou3lem2  26284  aaliou3lem8  26286  aaliou3lem5  26288  aaliou3lem6  26289  aaliou3lem7  26290  aaliou3  26292  sinperlem  26422  efimpi  26433  ptolemy  26438  sineq0  26466  efeq1  26470  tanregt0  26481  efif1olem2  26485  lognegb  26532  logneg2  26557  advlogexp  26597  logtayl  26602  logtayl2  26604  logccv  26605  cxpmul2z  26633  logbrec  26725  cosangneg2d  26750  isosctrlem2  26762  isosctrlem3  26763  angpined  26773  dcubic1lem  26786  dcubic2  26787  mcubic  26790  cubic2  26791  dquart  26796  quart1lem  26798  quartlem1  26800  quart  26804  asinlem3a  26813  asinneg  26829  atanneg  26850  atancj  26853  atanlogaddlem  26856  atanlogsublem  26858  atantan  26866  atantayl  26880  birthdaylem3  26896  amgmlem  26933  emcllem7  26945  lgamgulmlem2  26973  ftalem5  27020  basellem5  27028  basellem9  27032  lgsneg1  27266  lgseisenlem1  27319  lgseisenlem4  27322  m1lgs  27332  2sqblem  27375  dchrisum0flblem1  27452  rpvmasum2  27456  pntrsumo1  27509  pntrlog2bndlem2  27522  pntibndlem2  27535  padicfval  27560  padicval  27561  ostth3  27582  brbtwn2  28885  colinearalglem4  28889  axsegconlem9  28905  ex-ceil  30427  nvabs  30651  ipasslem2  30811  sgnval2  32708  re0cj  32717  argcj  32722  numdenneg  32789  archirngz  33158  elrgspnlem1  33209  ccfldextdgrr  33660  constrrtcc  33718  constrnegcl  33746  constrrecl  33752  cos9thpiminplylem1  33765  cos9thpiminplylem2  33766  xrge0iifcv  33917  xrge0iifhom  33920  xrge0iif1  33921  xrge0tmd  33928  xrge0tmdALT  33929  fdvneggt  34584  fdvnegge  34586  climlec3  35714  ditgeq123dv  36202  cbvditgdavw  36263  cbvditgdavw2  36279  dvtan  37657  itg2addnclem3  37660  ibladdnc  37664  ftc1anclem5  37684  ftc1anclem6  37685  areacirclem1  37695  areacirc  37700  dffltz  42615  3cubeslem3r  42668  pellexlem6  42815  pell1234qrdich  42842  rmxm1  42916  rmym1  42917  monotoddzzfi  42924  monotoddzz  42925  oddcomabszz  42926  acongeq12d  42961  acongeq  42965  sineq0ALT  44919  infnsuprnmpt  45237  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  48742  itsclc0yqsol  48746  itsclquadb  48758  itscnhlinecirc02plem2  48765  amgmwlem  49784