![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > negeqi | Structured version Visualization version GIF version |
Description: Equality inference for negatives. (Contributed by NM, 14-Feb-1995.) |
Ref | Expression |
---|---|
negeqi.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
negeqi | ⊢ -𝐴 = -𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | negeqi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | negeq 11448 | . 2 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ -𝐴 = -𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 -cneg 11441 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-rab 3425 df-v 3468 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-br 5139 df-iota 6485 df-fv 6541 df-ov 7404 df-neg 11443 |
This theorem is referenced by: negsubdii 11541 recgt0ii 12116 m1expcl2 14047 crreczi 14187 absi 15229 geo2sum2 15816 bpoly2 15997 bpoly3 15998 sinhval 16093 coshval 16094 cos2bnd 16127 divalglem2 16334 m1expaddsub 19403 cnmsgnsubg 21430 psgninv 21435 ncvspi 24994 cphipval2 25079 ditg0 25692 cbvditg 25693 ang180lem2 26646 ang180lem3 26647 ang180lem4 26648 1cubrlem 26677 dcubic2 26680 atandm2 26713 efiasin 26724 asinsinlem 26727 asinsin 26728 asin1 26730 reasinsin 26732 atancj 26746 atantayl2 26774 ppiub 27041 lgseisenlem1 27212 lgseisenlem2 27213 lgsquadlem1 27217 ostth3 27475 nvpi 30344 ipidsq 30387 ipasslem10 30516 normlem1 30787 polid2i 30834 lnophmlem2 31694 archirngz 32762 xrge0iif1 33373 ballotlem2 33942 itg2addnclem3 36997 dvasin 37028 areacirc 37037 lhe4.4ex1a 43543 itgsin0pilem1 45117 stoweidlem26 45193 dirkertrigeqlem3 45267 fourierdlem103 45376 sqwvfourb 45396 fourierswlem 45397 proththd 46733 |
Copyright terms: Public domain | W3C validator |