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 10880 | . 2 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ -𝐴 = -𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1537 -cneg 10873 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-rab 3149 df-v 3498 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-sn 4570 df-pr 4572 df-op 4576 df-uni 4841 df-br 5069 df-iota 6316 df-fv 6365 df-ov 7161 df-neg 10875 |
This theorem is referenced by: negsubdii 10973 recgt0ii 11548 m1expcl2 13454 crreczi 13592 absi 14648 geo2sum2 15232 bpoly2 15413 bpoly3 15414 sinhval 15509 coshval 15510 cos2bnd 15543 divalglem2 15748 m1expaddsub 18628 cnmsgnsubg 20723 psgninv 20728 ncvspi 23762 cphipval2 23846 ditg0 24453 cbvditg 24454 ang180lem2 25390 ang180lem3 25391 ang180lem4 25392 1cubrlem 25421 dcubic2 25424 atandm2 25457 efiasin 25468 asinsinlem 25471 asinsin 25472 asin1 25474 reasinsin 25476 atancj 25490 atantayl2 25518 ppiub 25782 lgseisenlem1 25953 lgseisenlem2 25954 lgsquadlem1 25958 ostth3 26216 nvpi 28446 ipidsq 28489 ipasslem10 28618 normlem1 28889 polid2i 28936 lnophmlem2 29796 archirngz 30820 xrge0iif1 31183 ballotlem2 31748 itg2addnclem3 34947 dvasin 34980 areacirc 34989 lhe4.4ex1a 40668 itgsin0pilem1 42242 stoweidlem26 42318 dirkertrigeqlem3 42392 fourierdlem103 42501 sqwvfourb 42521 fourierswlem 42522 proththd 43786 |
Copyright terms: Public domain | W3C validator |