Theorem negeqi 11377

Description: Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)

Hypothesis

Ref	Expression
negeqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
negeqi	⊢ -𝐴 = -𝐵

Proof of Theorem negeqi

Step	Hyp	Ref	Expression
1		negeqi.1	. 2 ⊢ 𝐴 = 𝐵
2		negeq 11376	. 2 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)
3	1, 2	ax-mp 5	1 ⊢ -𝐴 = -𝐵

Syntax hints:   = wceq 1547  -cneg 11369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359  df-neg 11371

This theorem is referenced by:  negsubdii  11470  recgt0ii  12053  m1expcl2  14038  crreczi  14181  absi  15239  geo2sum2  15830  bpoly2  16013  bpoly3  16014  sinhval  16112  coshval  16113  cos2bnd  16146  divalglem2  16355  m1expaddsub  19464  cnmsgnsubg  21552  psgninv  21557  ncvspi  25141  cphipval2  25226  ditg0  25838  cbvditg  25839  ang180lem2  26792  ang180lem3  26793  ang180lem4  26794  1cubrlem  26823  dcubic2  26826  atandm2  26859  efiasin  26870  asinsinlem  26873  asinsin  26874  asin1  26876  reasinsin  26878  atancj  26892  atantayl2  26920  ppiub  27185  lgseisenlem1  27356  lgseisenlem2  27357  lgsquadlem1  27361  ostth3  27619  nvpi  30756  ipidsq  30799  ipasslem10  30928  normlem1  31199  polid2i  31246  lnophmlem2  32106  archirngz  33270  cos9thpiminplylem1  33966  cos9thpiminplylem5  33970  xrge0iif1  34122  ballotlem2  34673  ditgeq123i  36437  cbvditgvw2  36477  itg2addnclem3  38040  dvasin  38071  areacirc  38080  cos2t3rdpi  42831  sin4t3rdpi  42832  cos4t3rdpi  42833  lhe4.4ex1a  44773  itgsin0pilem1  46393  stoweidlem26  46469  dirkertrigeqlem3  46543  fourierdlem103  46652  sqwvfourb  46672  fourierswlem  46673  proththd  48092