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

Theorem negeqd 10126
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 10124 . 2 (𝐴 = 𝐵 → -𝐴 = -𝐵)
31, 2syl 17 1 (𝜑 → -𝐴 = -𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  -cneg 10118
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530  df-neg 10120
This theorem is referenced by:  negdi  10189  mulneg2  10318  mulm1  10322  ltord2  10406  leord2  10407  eqord2  10408  divneg  10568  div2neg  10597  recgt0  10716  infrenegsup  10853  supminf  11607  mul2lt0rlt0  11764  ceilval  12456  dfceil2  12457  ceilid  12467  modcyc2  12523  monoord2  12649  expval  12679  discr  12818  reneg  13659  imneg  13667  cjcj  13674  cjneg  13681  sqeqd  13700  telfsumo2  14322  infcvgaux1i  14374  infcvgaux2i  14375  risefallfac  14540  bpoly3  14574  sinneg  14661  tanneg  14663  sincossq  14691  odd2np1  14849  oexpneg  14853  modgcd  15037  pcneg  15362  mulgval  17312  mulgneg  17329  psgnunilem2  17684  evth2  22498  ivth2  22948  mbfposb  23143  mbfinf  23155  mbfi1flimlem  23212  iblcnlem  23278  iblrelem  23280  itgrevallem1  23284  iblneg  23292  itgneg  23293  ibladd  23310  ditgeq1  23335  ditgeq2  23336  ditgeq3  23337  ditgneg  23344  ditgswap  23346  dvrec  23441  dvexp3  23462  dvsincos  23465  rolle  23474  dvivth  23494  dvfsumge  23506  dvfsumlem2  23511  dvfsum2  23518  ftc2ditg  23530  vieta1lem2  23787  vieta1  23788  aaliou3lem2  23819  aaliou3lem8  23821  aaliou3lem5  23823  aaliou3lem6  23824  aaliou3lem7  23825  aaliou3  23827  sinperlem  23953  efimpi  23964  ptolemy  23969  sineq0  23994  efeq1  23996  tanregt0  24006  efif1olem2  24010  lognegb  24057  logneg2  24082  advlogexp  24118  logtayl  24123  logtayl2  24125  logccv  24126  cxpmul2z  24154  logbrec  24237  cosangneg2d  24254  isosctrlem2  24266  isosctrlem3  24267  angpined  24274  dcubic1lem  24287  dcubic2  24288  mcubic  24291  cubic2  24292  dquart  24297  quart1lem  24299  quartlem1  24301  quart  24305  asinlem3a  24314  asinneg  24330  atanneg  24351  atancj  24354  atanlogaddlem  24357  atanlogsublem  24359  atantan  24367  atantayl  24381  birthdaylem3  24397  amgmlem  24433  emcllem7  24445  lgamgulmlem2  24473  ftalem5  24520  basellem5  24528  basellem9  24532  lgsneg1  24764  lgseisenlem1  24817  lgseisenlem4  24820  m1lgs  24830  2sqblem  24873  dchrisum0flblem1  24914  rpvmasum2  24918  pntrsumo1  24971  pntrlog2bndlem2  24984  pntibndlem2  24997  padicfval  25022  padicval  25023  ostth3  25044  brbtwn2  25503  colinearalglem4  25507  axsegconlem9  25523  ex-ceil  26463  nvabs  26706  ipasslem2  26877  numdenneg  28756  archirngz  28880  xrge0iifcv  29114  xrge0iifhom  29117  xrge0iif1  29118  xrge0tmdOLD  29125  xrge0tmd  29126  climlec3  30678  dvtan  32426  itg2addnclem3  32429  ibladdnc  32433  ftc1anclem5  32455  ftc1anclem6  32456  areacirclem1  32466  areacirc  32471  pellexlem6  36212  pell1234qrdich  36239  rmxm1  36313  rmym1  36314  monotoddzzfi  36321  monotoddzz  36322  oddcomabszz  36323  acongeq12d  36360  acongeq  36364  sineq0ALT  37991  neglimc  38511  dvrecg  38597  dvmptdiv  38604  dvcosax  38613  itgsin0pilem1  38638  itgsinexplem1  38642  itgsincmulx  38663  stoweidlem13  38703  stirlinglem5  38768  dirkerper  38786  dirkertrigeqlem3  38790  fourierdlem39  38836  fourierdlem40  38837  fourierdlem41  38838  fourierdlem43  38840  fourierdlem49  38845  fourierdlem73  38869  fourierdlem78  38874  fourierdlem103  38899  sqwvfourb  38919  etransclem46  38970  etransclem47  38971  sigarac  39487  sigaras  39490  sigarms  39491  sigariz  39498  sigarcol  39499  sharhght  39500  sigaradd  39501  2pwp1prm  39839  oexpnegALTV  39924  oexpnegnz  39925  amgmwlem  42313
  Copyright terms: Public domain W3C validator