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

Theorem negeqi 9232
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 9231 . 2  |-  ( A  =  B  ->  -u A  =  -u B )
31, 2ax-mp 8 1  |-  -u A  =  -u B
Colors of variables: wff set class
Syntax hints:    = wceq 1649   -ucneg 9225
This theorem is referenced by:  negsubdii  9318  recgt0ii  9849  m1expcl2  11331  crreczi  11432  absi  12019  geo2sum2  12579  sinhval  12683  coshval  12684  cos2bnd  12717  divalglem2  12843  ditg0  19608  cbvditg  19609  ang180lem2  20520  ang180lem3  20521  ang180lem4  20522  1cubrlem  20549  dcubic2  20552  atandm2  20585  efiasin  20596  asinsinlem  20599  asinsin  20600  asin1  20602  reasinsin  20604  atancj  20618  atantayl2  20646  ppiub  20856  lgseisenlem1  21001  lgseisenlem2  21002  lgsquadlem1  21006  ostth3  21200  nvpi  22004  ipidsq  22058  ipasslem10  22189  normlem1  22461  polid2i  22508  lnophmlem2  23369  xrge0iif1  24129  ballotlem2  24526  bpoly2  25818  bpoly3  25819  itg2addnc  25960  dvreasin  25981  areacirc  25989  m1expaddsub  27091  cnmsgnsubg  27104  lhe4.4ex1a  27216  itgsin0pilem1  27413  stoweidlem26  27444
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-rex 2656  df-rab 2659  df-v 2902  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-sn 3764  df-pr 3765  df-op 3767  df-uni 3959  df-br 4155  df-iota 5359  df-fv 5403  df-ov 6024  df-neg 9227
  Copyright terms: Public domain W3C validator