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

Theorem negeqd 10313
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 10311 . 2 (𝐴 = 𝐵 → -𝐴 = -𝐵)
31, 2syl 17 1 (𝜑 → -𝐴 = -𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  -cneg 10305
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-neg 10307
This theorem is referenced by:  negdi  10376  mulneg2  10505  mulm1  10509  ltord2  10595  leord2  10596  eqord2  10597  divneg  10757  div2neg  10786  recgt0  10905  infrenegsup  11044  supminf  11813  mul2lt0rlt0  11970  ceilval  12679  dfceil2  12680  ceilid  12690  modcyc2  12746  monoord2  12872  expval  12902  discr  13041  reneg  13909  imneg  13917  cjcj  13924  cjneg  13931  sqeqd  13950  telfsumo2  14579  infcvgaux1i  14633  infcvgaux2i  14634  risefallfac  14799  bpoly3  14833  sinneg  14920  tanneg  14922  sincossq  14950  odd2np1  15112  oexpneg  15116  modgcd  15300  pcneg  15625  mulgval  17590  mulgneg  17607  psgnunilem2  17961  evth2  22806  ivth2  23270  mbfposb  23465  mbfinf  23477  mbfi1flimlem  23534  iblcnlem  23600  iblrelem  23602  itgrevallem1  23606  iblneg  23614  itgneg  23615  ibladd  23632  ditgeq1  23657  ditgeq2  23658  ditgeq3  23659  ditgneg  23666  ditgswap  23668  dvrec  23763  dvrecg  23781  dvmptdiv  23782  dvexp3  23786  dvsincos  23789  rolle  23798  dvivth  23818  dvfsumge  23830  dvfsumlem2  23835  dvfsum2  23842  ftc2ditg  23854  vieta1lem2  24111  vieta1  24112  aaliou3lem2  24143  aaliou3lem8  24145  aaliou3lem5  24147  aaliou3lem6  24148  aaliou3lem7  24149  aaliou3  24151  sinperlem  24277  efimpi  24288  ptolemy  24293  sineq0  24318  efeq1  24320  tanregt0  24330  efif1olem2  24334  lognegb  24381  logneg2  24406  advlogexp  24446  logtayl  24451  logtayl2  24453  logccv  24454  cxpmul2z  24482  logbrec  24565  cosangneg2d  24582  isosctrlem2  24594  isosctrlem3  24595  angpined  24602  dcubic1lem  24615  dcubic2  24616  mcubic  24619  cubic2  24620  dquart  24625  quart1lem  24627  quartlem1  24629  quart  24633  asinlem3a  24642  asinneg  24658  atanneg  24679  atancj  24682  atanlogaddlem  24685  atanlogsublem  24687  atantan  24695  atantayl  24709  birthdaylem3  24725  amgmlem  24761  emcllem7  24773  lgamgulmlem2  24801  ftalem5  24848  basellem5  24856  basellem9  24860  lgsneg1  25092  lgseisenlem1  25145  lgseisenlem4  25148  m1lgs  25158  2sqblem  25201  dchrisum0flblem1  25242  rpvmasum2  25246  pntrsumo1  25299  pntrlog2bndlem2  25312  pntibndlem2  25325  padicfval  25350  padicval  25351  ostth3  25372  brbtwn2  25830  colinearalglem4  25834  axsegconlem9  25850  ex-ceil  27435  nvabs  27655  ipasslem2  27815  numdenneg  29691  archirngz  29871  xrge0iifcv  30108  xrge0iifhom  30111  xrge0iif1  30112  xrge0tmdOLD  30119  xrge0tmd  30120  fdvneggt  30806  fdvnegge  30808  climlec3  31745  dvtan  33590  itg2addnclem3  33593  ibladdnc  33597  ftc1anclem5  33619  ftc1anclem6  33620  areacirclem1  33630  areacirc  33635  pellexlem6  37715  pell1234qrdich  37742  rmxm1  37816  rmym1  37817  monotoddzzfi  37824  monotoddzz  37825  oddcomabszz  37826  acongeq12d  37863  acongeq  37867  sineq0ALT  39487  infnsuprnmpt  39779  supminfrnmpt  39985  supminfxr  40007  neglimc  40197  dvcosax  40459  itgsin0pilem1  40483  itgsinexplem1  40487  itgsincmulx  40508  stoweidlem13  40548  stirlinglem5  40613  dirkerper  40631  dirkertrigeqlem3  40635  fourierdlem39  40681  fourierdlem40  40682  fourierdlem41  40683  fourierdlem43  40685  fourierdlem49  40690  fourierdlem73  40714  fourierdlem78  40719  fourierdlem103  40744  sqwvfourb  40764  etransclem46  40815  etransclem47  40816  sigarac  41362  sigaras  41365  sigarms  41366  sigariz  41373  sigarcol  41374  sharhght  41375  sigaradd  41376  2pwp1prm  41828  oexpnegALTV  41913  oexpnegnz  41914  amgmwlem  42876
  Copyright terms: Public domain W3C validator