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

Theorem negeqi 10878
Description: Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)
Hypothesis
Ref Expression
negeqi.1 𝐴 = 𝐵
Assertion
Ref Expression
negeqi -𝐴 = -𝐵

Proof of Theorem negeqi
StepHypRef Expression
1 negeqi.1 . 2 𝐴 = 𝐵
2 negeq 10877 . 2 (𝐴 = 𝐵 → -𝐴 = -𝐵)
31, 2ax-mp 5 1 -𝐴 = -𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533  -cneg 10870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-iota 6313  df-fv 6362  df-ov 7158  df-neg 10872
This theorem is referenced by:  negsubdii  10970  recgt0ii  11545  m1expcl2  13450  crreczi  13588  absi  14645  geo2sum2  15229  bpoly2  15410  bpoly3  15411  sinhval  15506  coshval  15507  cos2bnd  15540  divalglem2  15745  m1expaddsub  18625  cnmsgnsubg  20720  psgninv  20725  ncvspi  23759  cphipval2  23843  ditg0  24450  cbvditg  24451  ang180lem2  25387  ang180lem3  25388  ang180lem4  25389  1cubrlem  25418  dcubic2  25421  atandm2  25454  efiasin  25465  asinsinlem  25468  asinsin  25469  asin1  25471  reasinsin  25473  atancj  25487  atantayl2  25515  ppiub  25779  lgseisenlem1  25950  lgseisenlem2  25951  lgsquadlem1  25955  ostth3  26213  nvpi  28443  ipidsq  28486  ipasslem10  28615  normlem1  28886  polid2i  28933  lnophmlem2  29793  archirngz  30818  xrge0iif1  31181  ballotlem2  31746  itg2addnclem3  34944  dvasin  34977  areacirc  34986  lhe4.4ex1a  40661  itgsin0pilem1  42235  stoweidlem26  42312  dirkertrigeqlem3  42386  fourierdlem103  42495  sqwvfourb  42515  fourierswlem  42516  proththd  43780
  Copyright terms: Public domain W3C validator