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

Theorem negeqi 9717
Description: Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)
Hypothesis
Ref Expression
negeqi.1  |-  A  =  B
Assertion
Ref Expression
negeqi  |-  -u A  =  -u B

Proof of Theorem negeqi
StepHypRef Expression
1 negeqi.1 . 2  |-  A  =  B
2 negeq 9716 . 2  |-  ( A  =  B  ->  -u A  =  -u B )
31, 2ax-mp 5 1  |-  -u A  =  -u B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370   -ucneg 9710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2805  df-rab 2808  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-br 4404  df-iota 5492  df-fv 5537  df-ov 6206  df-neg 9712
This theorem is referenced by:  negsubdii  9807  recgt0ii  10352  m1expcl2  12007  crreczi  12109  absi  12896  geo2sum2  13455  sinhval  13559  coshval  13560  cos2bnd  13593  divalglem2  13720  m1expaddsub  16126  cnmsgnsubg  18135  psgninv  18140  ditg0  21464  cbvditg  21465  ang180lem2  22342  ang180lem3  22343  ang180lem4  22344  1cubrlem  22372  dcubic2  22375  atandm2  22408  efiasin  22419  asinsinlem  22422  asinsin  22423  asin1  22425  reasinsin  22427  atancj  22441  atantayl2  22469  ppiub  22679  lgseisenlem1  22824  lgseisenlem2  22825  lgsquadlem1  22829  ostth3  23023  nvpi  24226  ipidsq  24280  ipasslem10  24411  normlem1  24684  polid2i  24731  lnophmlem2  25593  archirngz  26371  xrge0iif1  26533  ballotlem2  27035  bpoly2  28364  bpoly3  28365  itg2addnclem3  28613  dvasin  28648  areacirc  28657  lhe4.4ex1a  29771  itgsin0pilem1  29958  stoweidlem26  29989
  Copyright terms: Public domain W3C validator