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

Theorem negeqi 9812
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 9811 . 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 1379   -ucneg 9805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5550  df-fv 5595  df-ov 6286  df-neg 9807
This theorem is referenced by:  negsubdii  9903  recgt0ii  10450  m1expcl2  12155  crreczi  12258  absi  13081  geo2sum2  13645  sinhval  13749  coshval  13750  cos2bnd  13783  divalglem2  13911  m1expaddsub  16326  cnmsgnsubg  18396  psgninv  18401  ditg0  22008  cbvditg  22009  ang180lem2  22886  ang180lem3  22887  ang180lem4  22888  1cubrlem  22916  dcubic2  22919  atandm2  22952  efiasin  22963  asinsinlem  22966  asinsin  22967  asin1  22969  reasinsin  22971  atancj  22985  atantayl2  23013  ppiub  23223  lgseisenlem1  23368  lgseisenlem2  23369  lgsquadlem1  23373  ostth3  23567  nvpi  25261  ipidsq  25315  ipasslem10  25446  normlem1  25719  polid2i  25766  lnophmlem2  26628  archirngz  27411  xrge0iif1  27572  ballotlem2  28083  bpoly2  29412  bpoly3  29413  itg2addnclem3  29661  dvasin  29696  areacirc  29705  lhe4.4ex1a  30850  itgsin0pilem1  31283  stoweidlem26  31342  dirkertrigeqlem3  31416  fourierdlem103  31526  sqwvfourb  31546  fourierswlem  31547
  Copyright terms: Public domain W3C validator