![]() |
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 10593 | . 2 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ -𝐴 = -𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1658 -cneg 10586 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-rex 3123 df-rab 3126 df-v 3416 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4659 df-br 4874 df-iota 6086 df-fv 6131 df-ov 6908 df-neg 10588 |
This theorem is referenced by: negsubdii 10687 recgt0ii 11259 m1expcl2 13176 crreczi 13283 absi 14403 geo2sum2 14979 bpoly2 15160 bpoly3 15161 sinhval 15256 coshval 15257 cos2bnd 15290 divalglem2 15492 m1expaddsub 18269 cnmsgnsubg 20282 psgninv 20287 ncvspi 23325 cphipval2 23409 ditg0 24016 cbvditg 24017 ang180lem2 24950 ang180lem3 24951 ang180lem4 24952 1cubrlem 24981 dcubic2 24984 atandm2 25017 efiasin 25028 asinsinlem 25031 asinsin 25032 asin1 25034 reasinsin 25036 atancj 25050 atantayl2 25078 ppiub 25342 lgseisenlem1 25513 lgseisenlem2 25514 lgsquadlem1 25518 ostth3 25740 nvpi 28077 ipidsq 28120 ipasslem10 28249 normlem1 28522 polid2i 28569 lnophmlem2 29431 archirngz 30288 xrge0iif1 30529 ballotlem2 31096 itg2addnclem3 34006 dvasin 34039 areacirc 34048 lhe4.4ex1a 39368 itgsin0pilem1 40960 stoweidlem26 41037 dirkertrigeqlem3 41111 fourierdlem103 41220 sqwvfourb 41240 fourierswlem 41241 proththd 42361 |
Copyright terms: Public domain | W3C validator |