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

Theorem negeqd 9837
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 9835 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  -ucneg 9829
This theorem is referenced by:  negdi  9899  mulneg2  10019  mulm1  10023  ltord2  10107  leord2  10108  eqord2  10109  divneg  10264  div2neg  10292  recgt0  10411  infmsup  10546  supminf  11198  ceilval  11967  dfceil2  11968  ceilid  11978  modcyc2  12032  monoord2  12138  expval  12168  discr  12303  reneg  12958  imneg  12966  cjcj  12973  cjneg  12980  sqeqd  12999  telfsumo2  13617  infcvgaux1i  13668  infcvgaux2i  13669  sinneg  13881  tanneg  13883  sincossq  13911  odd2np1  14046  oexpneg  14049  modgcd  14174  pcneg  14397  mulgval  16144  mulgneg  16160  psgnunilem2  16520  evth2  21460  ivth2  21867  mbfposb  22060  mbfinf  22072  mbfi1flimlem  22129  iblcnlem  22195  iblrelem  22197  itgrevallem1  22201  iblneg  22209  itgneg  22210  ibladd  22227  ditgeq1  22252  ditgeq2  22253  ditgeq3  22254  ditgneg  22261  ditgswap  22263  dvrec  22358  dvexp3  22379  dvsincos  22382  rolle  22391  dvivth  22411  dvfsumge  22423  dvfsumlem2  22428  dvfsum2  22435  ftc2ditg  22447  vieta1lem2  22707  vieta1  22708  aaliou3lem2  22739  aaliou3lem8  22741  aaliou3lem5  22743  aaliou3lem6  22744  aaliou3lem7  22745  aaliou3  22747  sinperlem  22873  efimpi  22884  ptolemy  22889  sineq0  22914  efeq1  22916  tanregt0  22926  efif1olem2  22930  lognegb  22974  logneg2  23000  advlogexp  23036  logtayl  23041  logtayl2  23043  logccv  23044  cxpmul2z  23072  cosangneg2d  23139  isosctrlem2  23153  isosctrlem3  23154  angpined  23161  dcubic1lem  23174  dcubic2  23175  mcubic  23178  cubic2  23179  dquart  23184  quart1lem  23186  quartlem1  23188  quart  23192  asinlem3a  23201  asinneg  23217  atanneg  23238  atancj  23241  atanlogaddlem  23244  atanlogsublem  23246  atantan  23254  atantayl  23268  birthdaylem3  23283  amgmlem  23319  emcllem7  23331  ftalem5  23350  basellem5  23358  basellem9  23362  lgsneg1  23595  lgseisenlem1  23624  lgseisenlem4  23627  m1lgs  23637  2sqblem  23652  dchrisum0flblem1  23693  rpvmasum2  23697  pntrsumo1  23750  pntrlog2bndlem2  23763  pntibndlem2  23776  padicfval  23801  padicval  23802  ostth3  23823  brbtwn2  24208  colinearalglem4  24212  axsegconlem9  24228  nvabs  25576  ipasslem2  25747  mul2lt0rlt0  27565  numdenneg  27608  archirngz  27733  xrge0iifcv  27916  xrge0iifhom  27919  xrge0iif1  27920  xrge0tmdOLD  27927  xrge0tmd  27928  logbrec  28021  lgamgulmlem2  28572  climlec3  29120  risefallfac  29146  bpoly3  29820  dvtan  30065  itg2addnclem3  30068  ibladdnc  30072  ftc1anclem5  30094  ftc1anclem6  30095  areacirclem1  30107  areacirc  30112  pellexlem6  30770  pell1234qrdich  30797  rmxm1  30870  rmym1  30871  monotoddzzfi  30878  monotoddzz  30879  oddcomabszz  30880  acongeq12d  30917  acongeq  30921  neglimc  31653  dvrecg  31707  dvmptdiv  31714  dvcosax  31723  itgsin0pilem1  31748  itgsinexplem1  31752  itgsincmulx  31773  stoweidlem13  31795  stirlinglem5  31860  dirkerper  31878  dirkertrigeqlem3  31882  fourierdlem39  31928  fourierdlem40  31929  fourierdlem41  31930  fourierdlem43  31932  fourierdlem49  31938  fourierdlem73  31962  fourierdlem78  31967  fourierdlem103  31992  sqwvfourb  32012  etransclem46  32063  etransclem47  32064  sigarac  32069  sigaras  32072  sigarms  32073  sigariz  32080  sigarcol  32081  sharhght  32082  sigaradd  32083  sineq0ALT  33737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299  df-neg 9831
  Copyright terms: Public domain W3C validator