Theorem negeqd 11503

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

Syntax hints:   → wi 4   = wceq 1539  -cneg 11494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-iota 6513  df-fv 6568  df-ov 7435  df-neg 11496

This theorem is referenced by:  negdi  11567  mulneg2  11701  mulm1  11705  ltord2  11793  leord2  11794  eqord2  11795  divneg  11960  div2neg  11991  recgt0  12114  infrenegsup  12252  supminf  12978  mul2lt0rlt0  13138  ceilval  13879  dfceil2  13880  ceilid  13892  modcyc2  13948  monoord2  14075  expval  14105  discr  14280  reneg  15165  imneg  15173  cjcj  15180  cjneg  15187  sqeqd  15206  telfsumo2  15840  infcvgaux1i  15894  infcvgaux2i  15895  risefallfac  16061  bpoly3  16095  sinneg  16183  tanneg  16185  sincossq  16213  odd2np1  16379  oexpneg  16383  modgcd  16570  pcneg  16913  mulgval  19090  mulgneg  19111  psgnunilem2  19514  evth2  24993  ivth2  25491  mbfposb  25689  mbfinf  25701  mbfi1flimlem  25758  iblcnlem  25825  iblrelem  25827  itgrevallem1  25831  iblneg  25839  itgneg  25840  ibladd  25857  ditgeq1  25884  ditgeq2  25885  ditgeq3  25886  ditgneg  25893  ditgswap  25895  dvrec  25994  dvrecg  26012  dvmptdiv  26013  dvexp3  26017  dvsincos  26020  rolle  26029  dvivth  26050  dvfsumge  26063  dvfsumlem2  26068  dvfsumlem2OLD  26069  dvfsum2  26076  ftc2ditg  26088  vieta1lem2  26354  vieta1  26355  aaliou3lem2  26386  aaliou3lem8  26388  aaliou3lem5  26390  aaliou3lem6  26391  aaliou3lem7  26392  aaliou3  26394  sinperlem  26523  efimpi  26534  ptolemy  26539  sineq0  26567  efeq1  26571  tanregt0  26582  efif1olem2  26586  lognegb  26633  logneg2  26658  advlogexp  26698  logtayl  26703  logtayl2  26705  logccv  26706  cxpmul2z  26734  logbrec  26826  cosangneg2d  26851  isosctrlem2  26863  isosctrlem3  26864  angpined  26874  dcubic1lem  26887  dcubic2  26888  mcubic  26891  cubic2  26892  dquart  26897  quart1lem  26899  quartlem1  26901  quart  26905  asinlem3a  26914  asinneg  26930  atanneg  26951  atancj  26954  atanlogaddlem  26957  atanlogsublem  26959  atantan  26967  atantayl  26981  birthdaylem3  26997  amgmlem  27034  emcllem7  27046  lgamgulmlem2  27074  ftalem5  27121  basellem5  27129  basellem9  27133  lgsneg1  27367  lgseisenlem1  27420  lgseisenlem4  27423  m1lgs  27433  2sqblem  27476  dchrisum0flblem1  27553  rpvmasum2  27557  pntrsumo1  27610  pntrlog2bndlem2  27623  pntibndlem2  27636  padicfval  27661  padicval  27662  ostth3  27683  brbtwn2  28921  colinearalglem4  28925  axsegconlem9  28941  ex-ceil  30468  nvabs  30692  ipasslem2  30852  re0cj  32754  numdenneg  32817  archirngz  33197  elrgspnlem1  33247  ccfldextdgrr  33723  constrrtcc  33777  xrge0iifcv  33934  xrge0iifhom  33937  xrge0iif1  33938  xrge0tmd  33945  xrge0tmdALT  33946  fdvneggt  34616  fdvnegge  34618  climlec3  35735  ditgeq123dv  36223  cbvditgdavw  36284  cbvditgdavw2  36300  dvtan  37678  itg2addnclem3  37681  ibladdnc  37685  ftc1anclem5  37705  ftc1anclem6  37706  areacirclem1  37716  areacirc  37721  dffltz  42649  3cubeslem3r  42703  pellexlem6  42850  pell1234qrdich  42877  rmxm1  42951  rmym1  42952  monotoddzzfi  42959  monotoddzz  42960  oddcomabszz  42961  acongeq12d  42996  acongeq  43000  sineq0ALT  44962  infnsuprnmpt  45262  supminfrnmpt  45461  supminfxr  45480  neglimc  45667  dvcosax  45946  itgsin0pilem1  45970  itgsinexplem1  45974  itgsincmulx  45994  stoweidlem13  46033  stirlinglem5  46098  dirkerper  46116  dirkertrigeqlem3  46120  fourierdlem39  46166  fourierdlem40  46167  fourierdlem41  46168  fourierdlem43  46170  fourierdlem49  46175  fourierdlem73  46199  fourierdlem78  46204  fourierdlem103  46229  sqwvfourb  46249  etransclem46  46300  etransclem47  46301  sigarac  46872  sigaras  46875  sigarms  46876  sigariz  46883  sigarcol  46884  sharhght  46885  sigaradd  46886  ceildivmod  47346  2pwp1prm  47581  oexpnegALTV  47669  oexpnegnz  47670  itschlc0yqe  48686  itsclc0yqsol  48690  itsclquadb  48702  itscnhlinecirc02plem2  48709  amgmwlem  49376