Theorem negeqi 9836

Description: Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)

Hypothesis

Ref	Expression
negeqi.1

Assertion

Ref	Expression
negeqi

Proof of Theorem negeqi

Step	Hyp	Ref	Expression
1		negeqi.1	. 2
2		negeq 9835	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  =wceq 1395  -ucneg 9829

This theorem is referenced by:  negsubdii  9928  recgt0ii  10476  m1expcl2  12188  crreczi  12291  absi  13119  geo2sum2  13683  sinhval  13889  coshval  13890  cos2bnd  13923  divalglem2  14053  m1expaddsub  16523  cnmsgnsubg  18613  psgninv  18618  ditg0  22257  cbvditg  22258  ang180lem2  23142  ang180lem3  23143  ang180lem4  23144  1cubrlem  23172  dcubic2  23175  atandm2  23208  efiasin  23219  asinsinlem  23222  asinsin  23223  asin1  23225  reasinsin  23227  atancj  23241  atantayl2  23269  ppiub  23479  lgseisenlem1  23624  lgseisenlem2  23625  lgsquadlem1  23629  ostth3  23823  nvpi  25569  ipidsq  25623  ipasslem10  25754  normlem1  26027  polid2i  26074  lnophmlem2  26936  archirngz  27733  xrge0iif1  27920  ballotlem2  28427  bpoly2  29819  bpoly3  29820  itg2addnclem3  30068  dvasin  30103  areacirc  30112  lhe4.4ex1a  31234  itgsin0pilem1  31748  stoweidlem26  31808  dirkertrigeqlem3  31882  fourierdlem103  31992  sqwvfourb  32012  fourierswlem  32013

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