![]() |
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 10429 | . 2 ⊢ (𝐵 + 𝐴) = (𝐴 + 𝐵) |
4 | addcomli.2 | . 2 ⊢ (𝐴 + 𝐵) = 𝐶 | |
5 | 3, 4 | eqtri 2793 | 1 ⊢ (𝐵 + 𝐴) = 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1631 ∈ wcel 2145 (class class class)co 6793 ℂcc 10136 + caddc 10141 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4915 ax-nul 4923 ax-pow 4974 ax-pr 5034 ax-un 7096 ax-resscn 10195 ax-1cn 10196 ax-icn 10197 ax-addcl 10198 ax-addrcl 10199 ax-mulcl 10200 ax-mulrcl 10201 ax-mulcom 10202 ax-addass 10203 ax-mulass 10204 ax-distr 10205 ax-i2m1 10206 ax-1ne0 10207 ax-1rid 10208 ax-rnegex 10209 ax-rrecex 10210 ax-cnre 10211 ax-pre-lttri 10212 ax-pre-lttrn 10213 ax-pre-ltadd 10214 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 835 df-3or 1072 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-nel 3047 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-sbc 3588 df-csb 3683 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-nul 4064 df-if 4226 df-pw 4299 df-sn 4317 df-pr 4319 df-op 4323 df-uni 4575 df-br 4787 df-opab 4847 df-mpt 4864 df-id 5157 df-po 5170 df-so 5171 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262 df-iota 5994 df-fun 6033 df-fn 6034 df-f 6035 df-f1 6036 df-fo 6037 df-f1o 6038 df-fv 6039 df-ov 6796 df-er 7896 df-en 8110 df-dom 8111 df-sdom 8112 df-pnf 10278 df-mnf 10279 df-ltxr 10281 |
This theorem is referenced by: mvlladdi 10501 negsubdi2i 10569 1p2e3 11354 4t4e16 11834 6t3e18 11843 6t5e30 11845 6t5e30OLD 11846 7t3e21 11850 7t4e28 11851 7t6e42 11853 7t7e49 11854 8t3e24 11856 8t4e32 11857 8t5e40 11858 8t5e40OLD 11859 8t8e64 11863 9t3e27 11865 9t4e36 11866 9t5e45 11867 9t6e54 11868 9t7e63 11869 9t8e72 11870 9t9e81 11871 4bc3eq4 13319 n2dvdsm1 15313 bitsfzo 15365 gcdaddmlem 15453 6gcd4e2 15463 gcdi 15984 2exp8 16003 2exp16 16004 37prm 16035 43prm 16036 83prm 16037 139prm 16038 163prm 16039 317prm 16040 631prm 16041 1259lem1 16045 1259lem2 16046 1259lem3 16047 1259lem4 16048 1259lem5 16049 1259prm 16050 2503lem1 16051 2503lem2 16052 2503lem3 16053 2503prm 16054 4001lem1 16055 4001lem2 16056 4001lem4 16058 4001prm 16059 iaa 24300 dvradcnv 24395 eulerid 24447 binom4 24798 log2ublem3 24896 log2ub 24897 lgsdir2lem1 25271 m1lgs 25334 2lgsoddprmlem3d 25359 ex-bc 27651 ex-gcd 27656 ex-ind-dvds 27660 vcm 27771 fib5 30807 fib6 30808 hgt750lem 31069 hgt750lem2 31070 inductionexd 38979 lhe4.4ex1a 39054 dirkertrigeqlem1 40832 sqwvfoura 40962 sqwvfourb 40963 fourierswlem 40964 fouriersw 40965 fmtno5lem4 41996 257prm 42001 fmtno4nprmfac193 42014 fmtno5faclem3 42021 fmtno5fac 42022 139prmALT 42039 127prm 42043 gbpart8 42184 |
Copyright terms: Public domain | W3C validator |