Theorem negeqd 11446

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

Syntax hints:   → wi 4   = wceq 1570  -cneg 11437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-neg 11439

This theorem is referenced by:  negdi  11510  mulneg2  11646  mulm1  11650  ltord2  11738  leord2  11739  eqord2  11740  divneg  11901  div2neg  11933  recgt0  12056  infrenegsup  12193  supminf  12954  mul2lt0rlt0  13115  ceilval  13867  dfceil2  13868  ceilid  13880  modcyc2  13936  monoord2  14065  expval  14095  discr  14272  reneg  15172  imneg  15180  cjcj  15187  cjneg  15194  sqeqd  15213  telfsumo2  15851  infcvgaux1i  15907  infcvgaux2i  15908  risefallfac  16074  bpoly3  16107  sinneg  16197  tanneg  16199  sincossq  16227  odd2np1  16394  oexpneg  16398  modgcd  16585  pcneg  16929  mulgval  19132  mulgneg  19153  psgnunilem2  19560  evth2  25119  ivth2  25614  mbfposb  25812  mbfinf  25824  mbfi1flimlem  25881  iblcnlem  25948  iblrelem  25950  itgrevallem1  25954  iblneg  25962  itgneg  25963  ibladd  25980  ditgeq1  26007  ditgeq2  26008  ditgeq3  26009  ditgneg  26016  ditgswap  26018  dvrec  26114  dvrecg  26132  dvmptdiv  26133  dvexp3  26137  dvsincos  26140  rolle  26149  dvivth  26169  dvfsumge  26181  dvfsumlem2  26186  dvfsum2  26193  ftc2ditg  26205  vieta1lem2  26472  vieta1  26473  aaliou3lem2  26506  aaliou3lem8  26508  aaliou3lem5  26510  aaliou3lem6  26511  aaliou3lem7  26512  aaliou3  26514  aaliou3r  26515  sinperlem  26645  efimpi  26656  ptolemy  26661  sineq0  26689  efeq1  26693  tanregt0  26704  efif1olem2  26708  lognegb  26755  logneg2  26780  advlogexp  26820  logtayl  26825  logtayl2  26827  logccv  26828  cxpmul2z  26856  logbrec  26947  cosangneg2d  26972  isosctrlem2  26984  isosctrlem3  26985  angpined  26995  dcubic1lem  27008  dcubic2  27009  mcubic  27012  cubic2  27013  dquart  27018  quart1lem  27020  quartlem1  27022  quart  27026  asinlem3a  27035  asinneg  27051  atanneg  27072  atancj  27075  atanlogaddlem  27078  atanlogsublem  27080  atantan  27088  atantayl  27102  birthdaylem3  27118  amgmlem  27154  emcllem7  27166  lgamgulmlem2  27194  ftalem5  27241  basellem5  27249  basellem9  27253  lgsneg1  27486  lgseisenlem1  27539  lgseisenlem4  27542  m1lgs  27552  2sqblem  27595  dchrisum0flblem1  27672  rpvmasum2  27676  pntrsumo1  27729  pntrlog2bndlem2  27742  pntibndlem2  27755  padicfval  27780  padicval  27781  ostth3  27802  brbtwn2  29255  colinearalglem4  29259  axsegconlem9  29275  ex-ceil  30799  nvabs  31024  ipasslem2  31184  sgnval2  33080  re0cj  33088  argcj  33093  numdenneg  33159  archirngz  33509  elrgspnlem1  33562  ccfldextdgrr  34062  constrrtcc  34125  constrnegcl  34153  constrrecl  34159  cos9thpiminplylem1  34172  cos9thpiminplylem2  34173  xrge0iifcv  34324  xrge0iifhom  34327  xrge0iif1  34328  xrge0tmd  34335  xrge0tmdALT  34336  fdvneggt  34987  fdvnegge  34989  climlec3  36226  ditgeq123dv  36753  cbvditgdavw  36814  cbvditgdavw2  36830  dvtan  38341  itg2addnclem3  38344  ibladdnc  38348  ftc1anclem5  38368  ftc1anclem6  38369  areacirclem1  38379  areacirc  38384  25or6to4  42993  dffltz  43386  3cubeslem3r  43438  pellexlem6  43581  pell1234qrdich  43608  rmxm1  43681  rmym1  43682  monotoddzzfi  43689  monotoddzz  43690  oddcomabszz  43691  acongeq12d  43726  acongeq  43730  sineq0ALT  45665  infnsuprnmpt  45985  supminfrnmpt  46179  supminfxr  46198  neglimc  46381  dvcosax  46660  itgsin0pilem1  46684  itgsinexplem1  46688  itgsincmulx  46708  stoweidlem13  46747  stirlinglem5  46812  dirkerper  46830  dirkertrigeqlem3  46834  fourierdlem39  46880  fourierdlem40  46881  fourierdlem41  46882  fourierdlem43  46884  fourierdlem49  46889  fourierdlem73  46913  fourierdlem78  46918  fourierdlem103  46943  sqwvfourb  46963  etransclem46  47014  etransclem47  47015  sigarac  47586  sigaras  47589  sigarms  47590  sigariz  47597  sigarcol  47598  sharhght  47599  sigaradd  47600  ceildivmod  48102  difmodm1lt  48122  2pwp1prm  48361  oexpnegALTV  48462  oexpnegnz  48463  itschlc0yqe  49560  itsclc0yqsol  49564  itsclquadb  49576  itscnhlinecirc02plem2  49583  crosspalti  50667  amgmwlem  50669