Theorem negeqd 11468

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  -cneg 11459

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-neg 11461

This theorem is used by:  negdi  11532  mulneg2  11668  mulm1  11672  ltord2  11760  leord2  11761  eqord2  11762  divneg  11923  div2neg  11955  recgt0  12078  infrenegsup  12215  supminf  12977  mul2lt0rlt0  13138  ceilval  13891  dfceil2  13892  ceilid  13904  modcyc2  13960  monoord2  14089  expval  14119  discr  14296  reneg  15202  imneg  15210  cjcj  15217  cjneg  15224  sqeqd  15243  telfsumo2  15880  infcvgaux1i  15936  infcvgaux2i  15937  risefallfac  16103  bpoly3  16136  sinneg  16226  tanneg  16228  sincossq  16256  odd2np1  16423  oexpneg  16427  modgcd  16614  pcneg  16958  mulgval  19183  mulgneg  19204  psgnunilem2  19611  evth2  25172  ivth2  25667  mbfposb  25865  mbfinf  25877  mbfi1flimlem  25934  iblcnlem  26001  iblrelem  26003  itgrevallem1  26007  iblneg  26015  itgneg  26016  ibladd  26033  ditgeq1  26060  ditgeq2  26061  ditgeq3  26062  ditgneg  26069  ditgswap  26071  dvrec  26167  dvrecg  26185  dvmptdiv  26186  dvexp3  26190  dvsincos  26193  rolle  26202  dvivth  26222  dvfsumge  26234  dvfsumlem2  26239  dvfsum2  26246  ftc2ditg  26258  vieta1lem2  26525  vieta1  26526  aaliou3lem2  26559  aaliou3lem8  26561  aaliou3lem5  26563  aaliou3lem6  26564  aaliou3lem7  26565  aaliou3  26567  aaliou3r  26568  sinperlem  26698  efimpi  26709  ptolemy  26714  sineq0  26742  efeq1  26746  tanregt0  26757  efif1olem2  26761  lognegb  26808  logneg2  26833  advlogexp  26873  logtayl  26878  logtayl2  26880  logccv  26881  cxpmul2z  26909  logbrec  27000  cosangneg2d  27025  isosctrlem2  27037  isosctrlem3  27038  angpined  27048  dcubic1lem  27061  dcubic2  27062  mcubic  27065  cubic2  27066  dquart  27071  quart1lem  27073  quartlem1  27075  quart  27079  asinlem3a  27088  asinneg  27104  atanneg  27125  atancj  27128  atanlogaddlem  27131  atanlogsublem  27133  atantan  27141  atantayl  27155  birthdaylem3  27171  amgmlem  27207  emcllem7  27219  lgamgulmlem2  27247  ftalem5  27294  basellem5  27302  basellem9  27306  lgsneg1  27539  lgseisenlem1  27592  lgseisenlem4  27595  m1lgs  27605  2sqblem  27648  dchrisum0flblem1  27725  rpvmasum2  27729  pntrsumo1  27782  pntrlog2bndlem2  27795  pntibndlem2  27808  padicfval  27833  padicval  27834  ostth3  27855  brbtwn2  29312  colinearalglem4  29316  axsegconlem9  29332  ex-ceil  30872  nvabs  31097  ipasslem2  31257  sgnval2  33152  re0cj  33160  argcj  33165  numdenneg  33231  archirngz  33575  elrgspnlem1  33628  ccfldextdgrr  34128  constrrtcc  34191  constrnegcl  34219  constrrecl  34225  cos9thpiminplylem1  34238  cos9thpiminplylem2  34239  xrge0iifcv  34390  xrge0iifhom  34393  xrge0iif1  34394  xrge0tmd  34401  xrge0tmdALT  34402  fdvneggt  35054  fdvnegge  35056  climlec3  36265  ditgeq123dv  36792  cbvditgdavw  36853  cbvditgdavw2  36869  dvtan  38380  itg2addnclem3  38383  ibladdnc  38387  ftc1anclem5  38407  ftc1anclem6  38408  areacirclem1  38418  areacirc  38423  25or6to4  43033  dffltz  43426  3cubeslem3r  43478  pellexlem6  43621  pell1234qrdich  43648  rmxm1  43721  rmym1  43722  monotoddzzfi  43729  monotoddzz  43730  oddcomabszz  43731  acongeq12d  43766  acongeq  43770  sineq0ALT  45705  infnsuprnmpt  46025  supminfrnmpt  46219  supminfxr  46238  neglimc  46421  dvcosax  46700  itgsin0pilem1  46724  itgsinexplem1  46728  itgsincmulx  46748  stoweidlem13  46787  stirlinglem5  46852  dirkerper  46870  dirkertrigeqlem3  46874  fourierdlem39  46920  fourierdlem40  46921  fourierdlem41  46922  fourierdlem43  46924  fourierdlem49  46929  fourierdlem73  46953  fourierdlem78  46958  fourierdlem103  46983  sqwvfourb  47003  etransclem46  47054  etransclem47  47055  sigarac  47626  sigaras  47629  sigarms  47630  sigariz  47637  sigarcol  47638  sharhght  47639  sigaradd  47640  ceildivmod  48142  difmodm1lt  48162  2pwp1prm  48401  oexpnegALTV  48502  oexpnegnz  48503  itschlc0yqe  49599  itsclc0yqsol  49603  itsclquadb  49615  itscnhlinecirc02plem2  49622  crosspaltd  50707  amgmwlem  50709