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

Theorem negeqi 10259
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 10258 . 2 (𝐴 = 𝐵 → -𝐴 = -𝐵)
31, 2ax-mp 5 1 -𝐴 = -𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481  -cneg 10252
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-iota 5839  df-fv 5884  df-ov 6638  df-neg 10254
This theorem is referenced by:  negsubdii  10351  recgt0ii  10914  m1expcl2  12865  crreczi  12972  absi  14007  geo2sum2  14586  bpoly2  14769  bpoly3  14770  sinhval  14865  coshval  14866  cos2bnd  14899  divalglem2  15099  m1expaddsub  17899  cnmsgnsubg  19904  psgninv  19909  ncvspi  22937  cphipval2  23021  ditg0  23598  cbvditg  23599  ang180lem2  24521  ang180lem3  24522  ang180lem4  24523  1cubrlem  24549  dcubic2  24552  atandm2  24585  efiasin  24596  asinsinlem  24599  asinsin  24600  asin1  24602  reasinsin  24604  atancj  24618  atantayl2  24646  ppiub  24910  lgseisenlem1  25081  lgseisenlem2  25082  lgsquadlem1  25086  ostth3  25308  nvpi  27492  ipidsq  27535  ipasslem10  27664  normlem1  27937  polid2i  27984  lnophmlem2  28846  archirngz  29717  xrge0iif1  29958  ballotlem2  30524  itg2addnclem3  33434  dvasin  33467  areacirc  33476  lhe4.4ex1a  38348  itgsin0pilem1  39928  stoweidlem26  40006  dirkertrigeqlem3  40080  fourierdlem103  40189  sqwvfourb  40209  fourierswlem  40210  proththd  41296
  Copyright terms: Public domain W3C validator