Theorem negeqi 11560

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

This proof depends on syntax axioms:   = wceq 1569   -cneg 11552

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-iota 6500  df-fv 6554  df-ov 7430  df-neg 11554

This theorem is used by:  negsubdii  11653  recgt0ii  12233  m1expcl2  14238  crreczi  14382  absi  15465  geo2sum2  16055  bpoly2  16235  bpoly3  16236  sinhval  16334  coshval  16335  cos2bnd  16368  divalglem2  16577  m1expaddsub  19724  cnmsgnsubg  21895  psgninv  21900  ncvspi  25489  cphipval2  25574  ditg0  26185  cbvditg  26186  ang180lem2  27150  ang180lem3  27151  ang180lem4  27152  1cubrlem  27181  dcubic2  27184  atandm2  27217  efiasin  27228  asinsinlem  27231  asinsin  27232  asin1  27234  reasinsin  27236  atancj  27250  atantayl2  27278  ppiub  27543  lgseisenlem1  27714  lgseisenlem2  27715  lgsquadlem1  27719  ostth3  27977  nvpi  31281  ipidsq  31324  ipasslem10  31453  normlem1  31724  polid2i  31771  lnophmlem2  32631  archirngz  33803  cos9thpiminplylem1  34467  cos9thpiminplylem5  34471  xrge0iif1  34623  ballotlem2  35174  ditgeq123i  37125  cbvditgvw2  37165  itg2addnclem3  38731  dvasin  38762  areacirc  38771  25or6to4  43396  cos2t3rdpi  43545  sin4t3rdpi  43546  cos4t3rdpi  43547  lhe4.4ex1a  45453  itgsin0pilem1  47099  stoweidlem26  47175  dirkertrigeqlem3  47249  fourierdlem103  47358  sqwvfourb  47378  fourierswlem  47379  goldratval  48075  proththd  48838