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 10637 | . 2 ⊢ (𝐵 · 𝐴) = (𝐴 · 𝐵) |
4 | mulcomli.3 | . 2 ⊢ (𝐴 · 𝐵) = 𝐶 | |
5 | 3, 4 | eqtri 2841 | 1 ⊢ (𝐵 · 𝐴) = 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ∈ wcel 2105 (class class class)co 7145 ℂcc 10523 · cmul 10530 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-ext 2790 ax-mulcom 10589 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 |
This theorem is referenced by: divcan1i 11372 mvllmuli 11461 recgt0ii 11534 nummul2c 12136 halfthird 12229 5recm6rec 12230 sq4e2t8 13550 cos2bnd 15529 prmo3 16365 dec5nprm 16390 decexp2 16399 karatsuba 16408 2exp6 16410 2exp8 16411 2exp16 16412 7prm 16432 13prm 16437 17prm 16438 19prm 16439 23prm 16440 43prm 16443 83prm 16444 139prm 16445 163prm 16446 317prm 16447 631prm 16448 1259lem1 16452 1259lem2 16453 1259lem3 16454 1259lem4 16455 1259lem5 16456 1259prm 16457 2503lem1 16458 2503lem2 16459 2503lem3 16460 2503prm 16461 4001lem1 16462 4001lem2 16463 4001lem3 16464 4001lem4 16465 4001prm 16466 pcoass 23555 efif1olem2 25054 mcubic 25352 quart1lem 25360 quart1 25361 quartlem1 25362 tanatan 25424 log2ublem3 25453 log2ub 25454 cht3 25677 bclbnd 25783 bpos1lem 25785 bposlem4 25790 bposlem5 25791 bposlem8 25794 2lgslem3a 25899 2lgsoddprmlem3c 25915 2lgsoddprmlem3d 25916 ex-exp 28156 ex-fac 28157 ex-prmo 28165 ipasslem10 28543 siii 28557 normlem3 28816 bcsiALT 28883 dpmul1000 30502 hgt750lem2 31822 235t711 39055 ex-decpmul 39056 3cubeslem3l 39161 3cubeslem3r 39162 inductionexd 40383 fouriersw 42393 1t10e1p1e11 43387 fmtno5lem1 43592 fmtno5lem2 43593 257prm 43600 fmtno4prmfac 43611 fmtno4nprmfac193 43613 fmtno5faclem2 43619 139prmALT 43636 127prm 43640 2exp11 43642 mod42tp1mod8 43644 3exp4mod41 43658 41prothprmlem2 43660 2exp340mod341 43775 8exp8mod9 43778 |
Copyright terms: Public domain | W3C validator |