![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > addcomli | Structured version Visualization version GIF version |
Description: Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.) |
Ref | Expression |
---|---|
mul.1 | ⊢ 𝐴 ∈ ℂ |
mul.2 | ⊢ 𝐵 ∈ ℂ |
addcomli.2 | ⊢ (𝐴 + 𝐵) = 𝐶 |
Ref | Expression |
---|---|
addcomli | ⊢ (𝐵 + 𝐴) = 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mul.2 | . . 3 ⊢ 𝐵 ∈ ℂ | |
2 | mul.1 | . . 3 ⊢ 𝐴 ∈ ℂ | |
3 | 1, 2 | addcomi 10678 | . 2 ⊢ (𝐵 + 𝐴) = (𝐴 + 𝐵) |
4 | addcomli.2 | . 2 ⊢ (𝐴 + 𝐵) = 𝐶 | |
5 | 3, 4 | eqtri 2819 | 1 ⊢ (𝐵 + 𝐴) = 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1522 ∈ wcel 2081 (class class class)co 7016 ℂcc 10381 + caddc 10386 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 ax-resscn 10440 ax-1cn 10441 ax-icn 10442 ax-addcl 10443 ax-addrcl 10444 ax-mulcl 10445 ax-mulrcl 10446 ax-mulcom 10447 ax-addass 10448 ax-mulass 10449 ax-distr 10450 ax-i2m1 10451 ax-1ne0 10452 ax-1rid 10453 ax-rnegex 10454 ax-rrecex 10455 ax-cnre 10456 ax-pre-lttri 10457 ax-pre-lttrn 10458 ax-pre-ltadd 10459 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-nel 3091 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-opab 5025 df-mpt 5042 df-id 5348 df-po 5362 df-so 5363 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-f1 6230 df-fo 6231 df-f1o 6232 df-fv 6233 df-ov 7019 df-er 8139 df-en 8358 df-dom 8359 df-sdom 8360 df-pnf 10523 df-mnf 10524 df-ltxr 10526 |
This theorem is referenced by: mvlladdi 10752 negsubdi2i 10820 1p2e3ALT 11629 4t4e16 12047 6t3e18 12053 6t5e30 12055 7t3e21 12058 7t4e28 12059 7t6e42 12061 7t7e49 12062 8t3e24 12064 8t4e32 12065 8t5e40 12066 8t8e64 12069 9t3e27 12071 9t4e36 12072 9t5e45 12073 9t6e54 12074 9t7e63 12075 9t8e72 12076 9t9e81 12077 n2dvdsm1 15552 bitsfzo 15617 gcdaddmlem 15705 6gcd4e2 15715 gcdi 16238 2exp8 16252 2exp16 16253 37prm 16283 43prm 16284 83prm 16285 139prm 16286 163prm 16287 317prm 16288 631prm 16289 1259lem1 16293 1259lem2 16294 1259lem3 16295 1259lem4 16296 1259lem5 16297 1259prm 16298 2503lem1 16299 2503lem2 16300 2503lem3 16301 2503prm 16302 4001lem1 16303 4001lem2 16304 4001lem4 16306 4001prm 16307 iaa 24597 dvradcnv 24692 eulerid 24743 binom4 25109 log2ublem3 25208 log2ub 25209 lgsdir2lem1 25583 m1lgs 25646 2lgsoddprmlem3d 25671 addsqnreup 25701 ex-exp 27921 ex-bc 27923 ex-gcd 27928 ex-ind-dvds 27932 9p10ne21 27940 vcm 28044 fib5 31280 fib6 31281 hgt750lem 31539 hgt750lem2 31540 decpmulnc 38695 sqdeccom12 38697 sq3deccom12 38698 235t711 38699 ex-decpmul 38700 inductionexd 39990 lhe4.4ex1a 40199 dirkertrigeqlem1 41925 sqwvfoura 42055 sqwvfourb 42056 fourierswlem 42057 fouriersw 42058 fmtno5lem4 43200 257prm 43205 fmtno4nprmfac193 43218 fmtno5faclem3 43225 fmtno5fac 43226 139prmALT 43241 127prm 43245 11t31e341 43379 gbpart8 43415 |
Copyright terms: Public domain | W3C validator |