Theorem negeqi 11467

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

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

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-neg 11461

This theorem is used by:  negsubdii  11560  recgt0ii  12138  m1expcl2  14141  crreczi  14284  absi  15363  geo2sum2  15953  bpoly2  16135  bpoly3  16136  sinhval  16234  coshval  16235  cos2bnd  16268  divalglem2  16477  m1expaddsub  19614  cnmsgnsubg  21779  psgninv  21784  ncvspi  25368  cphipval2  25453  ditg0  26065  cbvditg  26066  ang180lem2  27028  ang180lem3  27029  ang180lem4  27030  1cubrlem  27059  dcubic2  27062  atandm2  27095  efiasin  27106  asinsinlem  27109  asinsin  27110  asin1  27112  reasinsin  27114  atancj  27128  atantayl2  27156  ppiub  27421  lgseisenlem1  27592  lgseisenlem2  27593  lgsquadlem1  27597  ostth3  27855  nvpi  31092  ipidsq  31135  ipasslem10  31264  normlem1  31535  polid2i  31582  lnophmlem2  32442  archirngz  33575  cos9thpiminplylem1  34238  cos9thpiminplylem5  34242  xrge0iif1  34394  ballotlem2  34946  ditgeq123i  36780  cbvditgvw2  36820  itg2addnclem3  38383  dvasin  38414  areacirc  38423  25or6to4  43033  cos2t3rdpi  43175  sin4t3rdpi  43176  cos4t3rdpi  43177  lhe4.4ex1a  45099  itgsin0pilem1  46724  stoweidlem26  46800  dirkertrigeqlem3  46874  fourierdlem103  46983  sqwvfourb  47003  fourierswlem  47004  proththd  48426