MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  negeqd Structured version   Visualization version   GIF version

Theorem negeqd 10459
Description: Equality deduction for negatives. (Contributed by NM, 14-May-1999.)
Hypothesis
Ref Expression
negeqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
negeqd (𝜑 → -𝐴 = -𝐵)

Proof of Theorem negeqd
StepHypRef Expression
1 negeqd.1 . 2 (𝜑𝐴 = 𝐵)
2 negeq 10457 . 2 (𝐴 = 𝐵 → -𝐴 = -𝐵)
31, 2syl 17 1 (𝜑 → -𝐴 = -𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1624  -cneg 10451
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rex 3048  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-iota 6004  df-fv 6049  df-ov 6808  df-neg 10453
This theorem is referenced by:  negdi  10522  mulneg2  10651  mulm1  10655  ltord2  10741  leord2  10742  eqord2  10743  divneg  10903  div2neg  10932  recgt0  11051  infrenegsup  11190  supminf  11960  mul2lt0rlt0  12117  ceilval  12825  dfceil2  12826  ceilid  12836  modcyc2  12892  monoord2  13018  expval  13048  discr  13187  reneg  14056  imneg  14064  cjcj  14071  cjneg  14078  sqeqd  14097  telfsumo2  14726  infcvgaux1i  14780  infcvgaux2i  14781  risefallfac  14946  bpoly3  14980  sinneg  15067  tanneg  15069  sincossq  15097  odd2np1  15259  oexpneg  15263  modgcd  15447  pcneg  15772  mulgval  17736  mulgneg  17753  psgnunilem2  18107  evth2  22952  ivth2  23416  mbfposb  23611  mbfinf  23623  mbfi1flimlem  23680  iblcnlem  23746  iblrelem  23748  itgrevallem1  23752  iblneg  23760  itgneg  23761  ibladd  23778  ditgeq1  23803  ditgeq2  23804  ditgeq3  23805  ditgneg  23812  ditgswap  23814  dvrec  23909  dvrecg  23927  dvmptdiv  23928  dvexp3  23932  dvsincos  23935  rolle  23944  dvivth  23964  dvfsumge  23976  dvfsumlem2  23981  dvfsum2  23988  ftc2ditg  24000  vieta1lem2  24257  vieta1  24258  aaliou3lem2  24289  aaliou3lem8  24291  aaliou3lem5  24293  aaliou3lem6  24294  aaliou3lem7  24295  aaliou3  24297  sinperlem  24423  efimpi  24434  ptolemy  24439  sineq0  24464  efeq1  24466  tanregt0  24476  efif1olem2  24480  lognegb  24527  logneg2  24552  advlogexp  24592  logtayl  24597  logtayl2  24599  logccv  24600  cxpmul2z  24628  logbrec  24711  cosangneg2d  24728  isosctrlem2  24740  isosctrlem3  24741  angpined  24748  dcubic1lem  24761  dcubic2  24762  mcubic  24765  cubic2  24766  dquart  24771  quart1lem  24773  quartlem1  24775  quart  24779  asinlem3a  24788  asinneg  24804  atanneg  24825  atancj  24828  atanlogaddlem  24831  atanlogsublem  24833  atantan  24841  atantayl  24855  birthdaylem3  24871  amgmlem  24907  emcllem7  24919  lgamgulmlem2  24947  ftalem5  24994  basellem5  25002  basellem9  25006  lgsneg1  25238  lgseisenlem1  25291  lgseisenlem4  25294  m1lgs  25304  2sqblem  25347  dchrisum0flblem1  25388  rpvmasum2  25392  pntrsumo1  25445  pntrlog2bndlem2  25458  pntibndlem2  25471  padicfval  25496  padicval  25497  ostth3  25518  brbtwn2  25976  colinearalglem4  25980  axsegconlem9  25996  ex-ceil  27608  nvabs  27828  ipasslem2  27988  numdenneg  29864  archirngz  30044  xrge0iifcv  30281  xrge0iifhom  30284  xrge0iif1  30285  xrge0tmdOLD  30292  xrge0tmd  30293  fdvneggt  30979  fdvnegge  30981  climlec3  31918  dvtan  33765  itg2addnclem3  33768  ibladdnc  33772  ftc1anclem5  33794  ftc1anclem6  33795  areacirclem1  33805  areacirc  33810  pellexlem6  37892  pell1234qrdich  37919  rmxm1  37993  rmym1  37994  monotoddzzfi  38001  monotoddzz  38002  oddcomabszz  38003  acongeq12d  38040  acongeq  38044  sineq0ALT  39664  infnsuprnmpt  39956  supminfrnmpt  40162  supminfxr  40184  neglimc  40374  dvcosax  40636  itgsin0pilem1  40660  itgsinexplem1  40664  itgsincmulx  40685  stoweidlem13  40725  stirlinglem5  40790  dirkerper  40808  dirkertrigeqlem3  40812  fourierdlem39  40858  fourierdlem40  40859  fourierdlem41  40860  fourierdlem43  40862  fourierdlem49  40867  fourierdlem73  40891  fourierdlem78  40896  fourierdlem103  40921  sqwvfourb  40941  etransclem46  40992  etransclem47  40993  sigarac  41539  sigaras  41542  sigarms  41543  sigariz  41550  sigarcol  41551  sharhght  41552  sigaradd  41553  2pwp1prm  42005  oexpnegALTV  42090  oexpnegnz  42091  amgmwlem  43053
  Copyright terms: Public domain W3C validator