Theorem negeqd 11530

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-neg 11523

This theorem is referenced by:  negdi  11593  mulneg2  11727  mulm1  11731  ltord2  11819  leord2  11820  eqord2  11821  divneg  11986  div2neg  12017  recgt0  12140  infrenegsup  12278  supminf  13000  mul2lt0rlt0  13159  ceilval  13889  dfceil2  13890  ceilid  13902  modcyc2  13958  monoord2  14084  expval  14114  discr  14289  reneg  15174  imneg  15182  cjcj  15189  cjneg  15196  sqeqd  15215  telfsumo2  15851  infcvgaux1i  15905  infcvgaux2i  15906  risefallfac  16072  bpoly3  16106  sinneg  16194  tanneg  16196  sincossq  16224  odd2np1  16389  oexpneg  16393  modgcd  16579  pcneg  16921  mulgval  19111  mulgneg  19132  psgnunilem2  19537  evth2  25011  ivth2  25509  mbfposb  25707  mbfinf  25719  mbfi1flimlem  25777  iblcnlem  25844  iblrelem  25846  itgrevallem1  25850  iblneg  25858  itgneg  25859  ibladd  25876  ditgeq1  25903  ditgeq2  25904  ditgeq3  25905  ditgneg  25912  ditgswap  25914  dvrec  26013  dvrecg  26031  dvmptdiv  26032  dvexp3  26036  dvsincos  26039  rolle  26048  dvivth  26069  dvfsumge  26082  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsum2  26095  ftc2ditg  26107  vieta1lem2  26371  vieta1  26372  aaliou3lem2  26403  aaliou3lem8  26405  aaliou3lem5  26407  aaliou3lem6  26408  aaliou3lem7  26409  aaliou3  26411  sinperlem  26540  efimpi  26551  ptolemy  26556  sineq0  26584  efeq1  26588  tanregt0  26599  efif1olem2  26603  lognegb  26650  logneg2  26675  advlogexp  26715  logtayl  26720  logtayl2  26722  logccv  26723  cxpmul2z  26751  logbrec  26843  cosangneg2d  26868  isosctrlem2  26880  isosctrlem3  26881  angpined  26891  dcubic1lem  26904  dcubic2  26905  mcubic  26908  cubic2  26909  dquart  26914  quart1lem  26916  quartlem1  26918  quart  26922  asinlem3a  26931  asinneg  26947  atanneg  26968  atancj  26971  atanlogaddlem  26974  atanlogsublem  26976  atantan  26984  atantayl  26998  birthdaylem3  27014  amgmlem  27051  emcllem7  27063  lgamgulmlem2  27091  ftalem5  27138  basellem5  27146  basellem9  27150  lgsneg1  27384  lgseisenlem1  27437  lgseisenlem4  27440  m1lgs  27450  2sqblem  27493  dchrisum0flblem1  27570  rpvmasum2  27574  pntrsumo1  27627  pntrlog2bndlem2  27640  pntibndlem2  27653  padicfval  27678  padicval  27679  ostth3  27700  brbtwn2  28938  colinearalglem4  28942  axsegconlem9  28958  ex-ceil  30480  nvabs  30704  ipasslem2  30864  re0cj  32756  numdenneg  32818  archirngz  33169  ccfldextdgrr  33682  constrrtcc  33726  xrge0iifcv  33880  xrge0iifhom  33883  xrge0iif1  33884  xrge0tmd  33891  xrge0tmdALT  33892  fdvneggt  34577  fdvnegge  34579  climlec3  35696  ditgeq123dv  36187  cbvditgdavw  36248  cbvditgdavw2  36264  dvtan  37630  itg2addnclem3  37633  ibladdnc  37637  ftc1anclem5  37657  ftc1anclem6  37658  areacirclem1  37668  areacirc  37673  dffltz  42589  3cubeslem3r  42643  pellexlem6  42790  pell1234qrdich  42817  rmxm1  42891  rmym1  42892  monotoddzzfi  42899  monotoddzz  42900  oddcomabszz  42901  acongeq12d  42936  acongeq  42940  sineq0ALT  44908  infnsuprnmpt  45159  supminfrnmpt  45360  supminfxr  45379  neglimc  45568  dvcosax  45847  itgsin0pilem1  45871  itgsinexplem1  45875  itgsincmulx  45895  stoweidlem13  45934  stirlinglem5  45999  dirkerper  46017  dirkertrigeqlem3  46021  fourierdlem39  46067  fourierdlem40  46068  fourierdlem41  46069  fourierdlem43  46071  fourierdlem49  46076  fourierdlem73  46100  fourierdlem78  46105  fourierdlem103  46130  sqwvfourb  46150  etransclem46  46201  etransclem47  46202  sigarac  46773  sigaras  46776  sigarms  46777  sigariz  46784  sigarcol  46785  sharhght  46786  sigaradd  46787  2pwp1prm  47463  oexpnegALTV  47551  oexpnegnz  47552  itschlc0yqe  48494  itsclc0yqsol  48498  itsclquadb  48510  itscnhlinecirc02plem2  48517  amgmwlem  48896