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 ⊢ -𝐴 = -𝐵

Syntax hints:   = wceq 1534  -cneg 11469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-iota 6494  df-fv 6550  df-ov 7417  df-neg 11471

This theorem is referenced by:  negsubdii  11569  recgt0ii  12144  m1expcl2  14076  crreczi  14216  absi  15259  geo2sum2  15846  bpoly2  16027  bpoly3  16028  sinhval  16124  coshval  16125  cos2bnd  16158  divalglem2  16365  m1expaddsub  19446  cnmsgnsubg  21502  psgninv  21507  ncvspi  25077  cphipval2  25162  ditg0  25775  cbvditg  25776  ang180lem2  26735  ang180lem3  26736  ang180lem4  26737  1cubrlem  26766  dcubic2  26769  atandm2  26802  efiasin  26813  asinsinlem  26816  asinsin  26817  asin1  26819  reasinsin  26821  atancj  26835  atantayl2  26863  ppiub  27130  lgseisenlem1  27301  lgseisenlem2  27302  lgsquadlem1  27306  ostth3  27564  nvpi  30470  ipidsq  30513  ipasslem10  30642  normlem1  30913  polid2i  30960  lnophmlem2  31820  archirngz  32891  xrge0iif1  33533  ballotlem2  34102  itg2addnclem3  37140  dvasin  37171  areacirc  37180  lhe4.4ex1a  43760  itgsin0pilem1  45332  stoweidlem26  45408  dirkertrigeqlem3  45482  fourierdlem103  45591  sqwvfourb  45611  fourierswlem  45612  proththd  46948

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »