Theorem negeqi 11550

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

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

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  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 6494  df-fv 6546  df-ov 7423  df-neg 11544

This theorem is used by:  negsubdii  11643  recgt0ii  12223  m1expcl2  14228  crreczi  14372  absi  15453  geo2sum2  16043  bpoly2  16223  bpoly3  16224  sinhval  16322  coshval  16323  cos2bnd  16356  divalglem2  16565  m1expaddsub  19712  cnmsgnsubg  21883  psgninv  21888  ncvspi  25477  cphipval2  25562  ditg0  26173  cbvditg  26174  ang180lem2  27138  ang180lem3  27139  ang180lem4  27140  1cubrlem  27169  dcubic2  27172  atandm2  27205  efiasin  27216  asinsinlem  27219  asinsin  27220  asin1  27222  reasinsin  27224  atancj  27238  atantayl2  27266  ppiub  27531  lgseisenlem1  27702  lgseisenlem2  27703  lgsquadlem1  27707  ostth3  27965  nvpi  31269  ipidsq  31312  ipasslem10  31441  normlem1  31712  polid2i  31759  lnophmlem2  32619  archirngz  33750  cos9thpiminplylem1  34414  cos9thpiminplylem5  34418  xrge0iif1  34570  ballotlem2  35121  ditgeq123i  36998  cbvditgvw2  37038  itg2addnclem3  38591  dvasin  38622  areacirc  38631  25or6to4  43256  cos2t3rdpi  43405  sin4t3rdpi  43406  cos4t3rdpi  43407  lhe4.4ex1a  45312  itgsin0pilem1  46959  stoweidlem26  47035  dirkertrigeqlem3  47109  fourierdlem103  47218  sqwvfourb  47238  fourierswlem  47239  goldratval  47935  proththd  48698