Theorem negeqi 10873

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

Syntax hints:   = wceq 1533  -cneg 10865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-iota 6309  df-fv 6358  df-ov 7153  df-neg 10867

This theorem is referenced by:  negsubdii  10965  recgt0ii  11540  m1expcl2  13445  crreczi  13583  absi  14640  geo2sum2  15224  bpoly2  15405  bpoly3  15406  sinhval  15501  coshval  15502  cos2bnd  15535  divalglem2  15740  m1expaddsub  18620  cnmsgnsubg  20715  psgninv  20720  ncvspi  23754  cphipval2  23838  ditg0  24445  cbvditg  24446  ang180lem2  25382  ang180lem3  25383  ang180lem4  25384  1cubrlem  25413  dcubic2  25416  atandm2  25449  efiasin  25460  asinsinlem  25463  asinsin  25464  asin1  25466  reasinsin  25468  atancj  25482  atantayl2  25510  ppiub  25774  lgseisenlem1  25945  lgseisenlem2  25946  lgsquadlem1  25950  ostth3  26208  nvpi  28438  ipidsq  28481  ipasslem10  28610  normlem1  28881  polid2i  28928  lnophmlem2  29788  archirngz  30813  xrge0iif1  31176  ballotlem2  31741  itg2addnclem3  34939  dvasin  34972  areacirc  34981  lhe4.4ex1a  40654  itgsin0pilem1  42227  stoweidlem26  42304  dirkertrigeqlem3  42378  fourierdlem103  42487  sqwvfourb  42507  fourierswlem  42508  proththd  43772