Theorem negeqd 11481

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-neg 11474

This theorem is referenced by:  negdi  11545  mulneg2  11679  mulm1  11683  ltord2  11771  leord2  11772  eqord2  11773  divneg  11938  div2neg  11969  recgt0  12092  infrenegsup  12230  supminf  12956  mul2lt0rlt0  13116  ceilval  13860  dfceil2  13861  ceilid  13873  modcyc2  13929  monoord2  14056  expval  14086  discr  14263  reneg  15149  imneg  15157  cjcj  15164  cjneg  15171  sqeqd  15190  telfsumo2  15824  infcvgaux1i  15878  infcvgaux2i  15879  risefallfac  16045  bpoly3  16079  sinneg  16169  tanneg  16171  sincossq  16199  odd2np1  16365  oexpneg  16369  modgcd  16556  pcneg  16899  mulgval  19059  mulgneg  19080  psgnunilem2  19481  evth2  24915  ivth2  25413  mbfposb  25611  mbfinf  25623  mbfi1flimlem  25680  iblcnlem  25747  iblrelem  25749  itgrevallem1  25753  iblneg  25761  itgneg  25762  ibladd  25779  ditgeq1  25806  ditgeq2  25807  ditgeq3  25808  ditgneg  25815  ditgswap  25817  dvrec  25916  dvrecg  25934  dvmptdiv  25935  dvexp3  25939  dvsincos  25942  rolle  25951  dvivth  25972  dvfsumge  25985  dvfsumlem2  25990  dvfsumlem2OLD  25991  dvfsum2  25998  ftc2ditg  26010  vieta1lem2  26276  vieta1  26277  aaliou3lem2  26308  aaliou3lem8  26310  aaliou3lem5  26312  aaliou3lem6  26313  aaliou3lem7  26314  aaliou3  26316  sinperlem  26446  efimpi  26457  ptolemy  26462  sineq0  26490  efeq1  26494  tanregt0  26505  efif1olem2  26509  lognegb  26556  logneg2  26581  advlogexp  26621  logtayl  26626  logtayl2  26628  logccv  26629  cxpmul2z  26657  logbrec  26749  cosangneg2d  26774  isosctrlem2  26786  isosctrlem3  26787  angpined  26797  dcubic1lem  26810  dcubic2  26811  mcubic  26814  cubic2  26815  dquart  26820  quart1lem  26822  quartlem1  26824  quart  26828  asinlem3a  26837  asinneg  26853  atanneg  26874  atancj  26877  atanlogaddlem  26880  atanlogsublem  26882  atantan  26890  atantayl  26904  birthdaylem3  26920  amgmlem  26957  emcllem7  26969  lgamgulmlem2  26997  ftalem5  27044  basellem5  27052  basellem9  27056  lgsneg1  27290  lgseisenlem1  27343  lgseisenlem4  27346  m1lgs  27356  2sqblem  27399  dchrisum0flblem1  27476  rpvmasum2  27480  pntrsumo1  27533  pntrlog2bndlem2  27546  pntibndlem2  27559  padicfval  27584  padicval  27585  ostth3  27606  brbtwn2  28889  colinearalglem4  28893  axsegconlem9  28909  ex-ceil  30434  nvabs  30658  ipasslem2  30818  sgnval2  32717  re0cj  32726  argcj  32731  numdenneg  32798  archirngz  33192  elrgspnlem1  33242  ccfldextdgrr  33718  constrrtcc  33774  constrnegcl  33802  constrrecl  33808  cos9thpiminplylem1  33821  cos9thpiminplylem2  33822  xrge0iifcv  33970  xrge0iifhom  33973  xrge0iif1  33974  xrge0tmd  33981  xrge0tmdALT  33982  fdvneggt  34637  fdvnegge  34639  climlec3  35756  ditgeq123dv  36244  cbvditgdavw  36305  cbvditgdavw2  36321  dvtan  37699  itg2addnclem3  37702  ibladdnc  37706  ftc1anclem5  37726  ftc1anclem6  37727  areacirclem1  37737  areacirc  37742  dffltz  42632  3cubeslem3r  42685  pellexlem6  42832  pell1234qrdich  42859  rmxm1  42933  rmym1  42934  monotoddzzfi  42941  monotoddzz  42942  oddcomabszz  42943  acongeq12d  42978  acongeq  42982  sineq0ALT  44936  infnsuprnmpt  45254  supminfrnmpt  45452  supminfxr  45471  neglimc  45656  dvcosax  45935  itgsin0pilem1  45959  itgsinexplem1  45963  itgsincmulx  45983  stoweidlem13  46022  stirlinglem5  46087  dirkerper  46105  dirkertrigeqlem3  46109  fourierdlem39  46155  fourierdlem40  46156  fourierdlem41  46157  fourierdlem43  46159  fourierdlem49  46164  fourierdlem73  46188  fourierdlem78  46193  fourierdlem103  46218  sqwvfourb  46238  etransclem46  46289  etransclem47  46290  sigarac  46861  sigaras  46864  sigarms  46865  sigariz  46872  sigarcol  46873  sharhght  46874  sigaradd  46875  ceildivmod  47348  2pwp1prm  47583  oexpnegALTV  47671  oexpnegnz  47672  itschlc0yqe  48720  itsclc0yqsol  48724  itsclquadb  48736  itscnhlinecirc02plem2  48743  amgmwlem  49646