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

Theorem negeqi 10312
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 10311 . 2 (𝐴 = 𝐵 → -𝐴 = -𝐵)
31, 2ax-mp 5 1 -𝐴 = -𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  -cneg 10305
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-neg 10307
This theorem is referenced by:  negsubdii  10404  recgt0ii  10967  m1expcl2  12922  crreczi  13029  absi  14070  geo2sum2  14649  bpoly2  14832  bpoly3  14833  sinhval  14928  coshval  14929  cos2bnd  14962  divalglem2  15165  m1expaddsub  17964  cnmsgnsubg  19971  psgninv  19976  ncvspi  23002  cphipval2  23086  ditg0  23662  cbvditg  23663  ang180lem2  24585  ang180lem3  24586  ang180lem4  24587  1cubrlem  24613  dcubic2  24616  atandm2  24649  efiasin  24660  asinsinlem  24663  asinsin  24664  asin1  24666  reasinsin  24668  atancj  24682  atantayl2  24710  ppiub  24974  lgseisenlem1  25145  lgseisenlem2  25146  lgsquadlem1  25150  ostth3  25372  nvpi  27650  ipidsq  27693  ipasslem10  27822  normlem1  28095  polid2i  28142  lnophmlem2  29004  archirngz  29871  xrge0iif1  30112  ballotlem2  30678  itg2addnclem3  33593  dvasin  33626  areacirc  33635  lhe4.4ex1a  38845  itgsin0pilem1  40483  stoweidlem26  40561  dirkertrigeqlem3  40635  fourierdlem103  40744  sqwvfourb  40764  fourierswlem  40765  proththd  41856
  Copyright terms: Public domain W3C validator