Theorem negeqi 11477

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 11476	. 2 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)
3	1, 2	ax-mp 5	1 ⊢ -𝐴 = -𝐵

This proof depends on syntax axioms:   = wceq 1570  -cneg 11469

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417  df-neg 11471

This theorem is used by:  negsubdii  11570  recgt0ii  12148  m1expcl2  14152  crreczi  14295  absi  15376  geo2sum2  15966  bpoly2  16146  bpoly3  16147  sinhval  16245  coshval  16246  cos2bnd  16279  divalglem2  16488  m1expaddsub  19628  cnmsgnsubg  21793  psgninv  21798  ncvspi  25387  cphipval2  25472  ditg0  26083  cbvditg  26084  ang180lem2  27050  ang180lem3  27051  ang180lem4  27052  1cubrlem  27081  dcubic2  27084  atandm2  27117  efiasin  27128  asinsinlem  27131  asinsin  27132  asin1  27134  reasinsin  27136  atancj  27150  atantayl2  27178  ppiub  27443  lgseisenlem1  27614  lgseisenlem2  27615  lgsquadlem1  27619  ostth3  27877  nvpi  31151  ipidsq  31194  ipasslem10  31323  normlem1  31594  polid2i  31641  lnophmlem2  32501  archirngz  33632  cos9thpiminplylem1  34295  cos9thpiminplylem5  34299  xrge0iif1  34451  ballotlem2  35003  ditgeq123i  36832  cbvditgvw2  36872  itg2addnclem3  38425  dvasin  38456  areacirc  38465  25or6to4  43075  cos2t3rdpi  43232  sin4t3rdpi  43233  cos4t3rdpi  43234  lhe4.4ex1a  45156  itgsin0pilem1  46781  stoweidlem26  46857  dirkertrigeqlem3  46931  fourierdlem103  47040  sqwvfourb  47060  fourierswlem  47061  goldratval  47757  proththd  48520