Theorem negeqd 11561

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   -cneg 11552

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-iota 6500  df-fv 6554  df-ov 7430  df-neg 11554

This theorem is used by:  negdi  11625  mulneg2  11763  mulm1  11767  ltord2  11855  leord2  11856  eqord2  11857  divneg  12018  div2neg  12050  recgt0  12173  infrenegsup  12310  supminf  13072  mul2lt0rlt0  13234  ceilval  13988  dfceil2  13989  ceilid  14001  modcyc2  14057  monoord2  14186  expval  14216  discr  14394  reneg  15304  imneg  15312  cjcj  15319  cjneg  15326  sqeqd  15345  telfsumo2  15982  infcvgaux1i  16038  infcvgaux2i  16039  risefallfac  16203  bpoly3  16236  sinneg  16326  tanneg  16328  sincossq  16356  odd2np1  16523  oexpneg  16527  modgcd  16717  pcneg  17064  mulgval  19293  mulgneg  19314  psgnunilem2  19721  evth2  25293  ivth2  25788  mbfposb  25986  mbfinf  25998  mbfi1flimlem  26055  iblcnlem  26121  iblrelem  26123  itgrevallem1  26127  iblneg  26135  itgneg  26136  ibladd  26153  ditgeq1  26180  ditgeq2  26181  ditgeq3  26182  ditgneg  26189  ditgswap  26191  dvrec  26287  dvrecg  26305  dvmptdiv  26306  dvexp3  26310  dvsincos  26313  rolle  26322  dvivth  26342  dvfsumge  26354  dvfsumlem2  26359  dvfsum2  26366  ftc2ditg  26378  vieta1lem2  26646  vieta1  26647  aaliou3lem2  26682  aaliou3lem8  26684  aaliou3lem5  26686  aaliou3lem6  26687  aaliou3lem7  26688  aaliou3  26690  aaliou3r  26691  sinperlem  26821  efimpi  26832  ptolemy  26837  sineq0  26864  efeq1  26868  tanregt0  26879  efif1olem2  26883  lognegb  26930  logneg2  26955  advlogexp  26995  logtayl  27000  logtayl2  27002  logccv  27003  cxpmul2z  27031  logbrec  27122  cosangneg2d  27147  isosctrlem2  27159  isosctrlem3  27160  angpined  27170  dcubic1lem  27183  dcubic2  27184  mcubic  27187  cubic2  27188  dquart  27193  quart1lem  27195  quartlem1  27197  quart  27201  asinlem3a  27210  asinneg  27226  atanneg  27247  atancj  27250  atanlogaddlem  27253  atanlogsublem  27255  atantan  27263  atantayl  27277  birthdaylem3  27293  amgmlem  27329  emcllem7  27341  lgamgulmlem2  27369  ftalem5  27416  basellem5  27424  basellem9  27428  lgsneg1  27661  lgseisenlem1  27714  lgseisenlem4  27717  m1lgs  27727  2sqblem  27770  dchrisum0flblem1  27847  rpvmasum2  27851  pntrsumo1  27904  pntrlog2bndlem2  27917  pntibndlem2  27930  padicfval  27955  padicval  27956  ostth3  27977  brbtwn2  29495  colinearalglem4  29499  axsegconlem9  29515  ex-ceil  31061  nvabs  31286  ipasslem2  31446  sgnval2  33380  re0cj  33388  argcj  33393  numdenneg  33459  archirngz  33803  elrgspnlem1  33856  ccfldextdgrr  34357  constrrtcc  34420  constrnegcl  34448  constrrecl  34454  cos9thpiminplylem1  34467  cos9thpiminplylem2  34468  xrge0iifcv  34619  xrge0iifhom  34622  xrge0iif1  34623  xrge0tmd  34630  xrge0tmdALT  34631  fdvneggt  35282  fdvnegge  35284  climlec3  36626  ditgeq123dv  37137  cbvditgdavw  37198  cbvditgdavw2  37214  dvtan  38728  itg2addnclem3  38731  ibladdnc  38735  ftc1anclem5  38755  ftc1anclem6  38756  areacirclem1  38766  areacirc  38771  25or6to4  43396  dffltz  43810  3cubeslem3r  43837  pellexlem6  43981  pell1234qrdich  44008  rmxm1  44081  rmym1  44082  monotoddzzfi  44089  monotoddzz  44090  oddcomabszz  44091  acongeq12d  44126  acongeq  44130  sineq0ALT  46058  infnsuprnmpt  46401  supminfrnmpt  46594  supminfxr  46613  neglimc  46796  dvcosax  47075  itgsin0pilem1  47099  itgsinexplem1  47103  itgsincmulx  47123  stoweidlem13  47162  stirlinglem5  47227  dirkerper  47245  dirkertrigeqlem3  47249  fourierdlem39  47295  fourierdlem40  47296  fourierdlem41  47297  fourierdlem43  47299  fourierdlem49  47304  fourierdlem73  47328  fourierdlem78  47333  fourierdlem103  47358  sqwvfourb  47378  etransclem46  47429  etransclem47  47430  sigarac  48001  sigaras  48004  sigarms  48005  sigariz  48012  sigarcol  48013  sharhght  48014  sigaradd  48015  ceildivmod  48554  difmodm1lt  48574  2pwp1prm  48813  oexpnegALTV  48914  oexpnegnz  48915  itschlc0yqe  50011  itsclc0yqsol  50015  itsclquadb  50027  itscnhlinecirc02plem2  50034  dvsec  51070  dvcsc  51071  dvcot  51072  crosspaltd  51180  amgmwlem  51201