![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mulcomli | Structured version Visualization version GIF version |
Description: Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Ref | Expression |
---|---|
axi.1 | ⊢ 𝐴 ∈ ℂ |
axi.2 | ⊢ 𝐵 ∈ ℂ |
mulcomli.3 | ⊢ (𝐴 · 𝐵) = 𝐶 |
Ref | Expression |
---|---|
mulcomli | ⊢ (𝐵 · 𝐴) = 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axi.2 | . . 3 ⊢ 𝐵 ∈ ℂ | |
2 | axi.1 | . . 3 ⊢ 𝐴 ∈ ℂ | |
3 | 1, 2 | mulcomi 10450 | . 2 ⊢ (𝐵 · 𝐴) = (𝐴 · 𝐵) |
4 | mulcomli.3 | . 2 ⊢ (𝐴 · 𝐵) = 𝐶 | |
5 | 3, 4 | eqtri 2802 | 1 ⊢ (𝐵 · 𝐴) = 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1507 ∈ wcel 2050 (class class class)co 6978 ℂcc 10335 · cmul 10342 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-9 2059 ax-ext 2750 ax-mulcom 10401 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-cleq 2771 |
This theorem is referenced by: divcan1i 11187 mvllmuli 11276 recgt0ii 11349 nummul2c 11965 halfthird 12059 5recm6rec 12060 sq4e2t8 13380 cos2bnd 15404 prmo3 16236 dec5nprm 16261 decexp2 16270 karatsuba 16279 2exp6 16281 2exp8 16282 2exp16 16283 7prm 16303 13prm 16308 17prm 16309 19prm 16310 23prm 16311 43prm 16314 83prm 16315 139prm 16316 163prm 16317 317prm 16318 631prm 16319 1259lem1 16323 1259lem2 16324 1259lem3 16325 1259lem4 16326 1259lem5 16327 1259prm 16328 2503lem1 16329 2503lem2 16330 2503lem3 16331 2503prm 16332 4001lem1 16333 4001lem2 16334 4001lem3 16335 4001lem4 16336 4001prm 16337 pcoass 23334 efif1olem2 24831 mcubic 25129 quart1lem 25137 quart1 25138 quartlem1 25139 tanatan 25201 log2ublem3 25231 log2ub 25232 cht3 25455 bclbnd 25561 bpos1lem 25563 bposlem4 25568 bposlem5 25569 bposlem8 25572 2lgslem3a 25677 2lgsoddprmlem3c 25693 2lgsoddprmlem3d 25694 ex-exp 28010 ex-fac 28011 ex-prmo 28019 ipasslem10 28396 siii 28410 normlem3 28671 bcsiALT 28738 dpmul1000 30324 hgt750lem2 31571 235t711 38609 ex-decpmul 38610 inductionexd 39868 fouriersw 41948 1t10e1p1e11 42917 fmtno5lem1 43084 fmtno5lem2 43085 257prm 43092 fmtno4prmfac 43103 fmtno4nprmfac193 43105 fmtno5faclem2 43111 139prmALT 43128 127prm 43132 2exp11 43134 mod42tp1mod8 43136 3exp4mod41 43150 41prothprmlem2 43152 2exp340mod341 43267 8exp8mod9 43270 |
Copyright terms: Public domain | W3C validator |