| 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 11269 | . 2 ⊢ (𝐵 · 𝐴) = (𝐴 · 𝐵) |
| 4 | mulcomli.3 | . 2 ⊢ (𝐴 · 𝐵) = 𝐶 | |
| 5 | 3, 4 | eqtri 2765 | 1 ⊢ (𝐵 · 𝐴) = 𝐶 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∈ wcel 2108 (class class class)co 7431 ℂcc 11153 · cmul 11160 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 ax-mulcom 11219 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 |
| This theorem is referenced by: divcan1i 12011 mvllmuli 12100 recgt0ii 12174 nummul2c 12783 halfthird 12876 5recm6rec 12877 sq4e2t8 14238 cos2bnd 16224 prmo3 17079 dec5nprm 17104 karatsuba 17121 2exp6 17124 2exp8 17126 2exp11 17127 2exp16 17128 7prm 17148 13prm 17153 17prm 17154 19prm 17155 23prm 17156 43prm 17159 83prm 17160 139prm 17161 163prm 17162 317prm 17163 631prm 17164 1259lem1 17168 1259lem2 17169 1259lem3 17170 1259lem4 17171 1259lem5 17172 1259prm 17173 2503lem1 17174 2503lem2 17175 2503lem3 17176 2503prm 17177 4001lem1 17178 4001lem2 17179 4001lem3 17180 4001lem4 17181 4001prm 17182 pcoass 25057 efif1olem2 26585 mcubic 26890 quart1lem 26898 quart1 26899 quartlem1 26900 tanatan 26962 log2ublem3 26991 log2ub 26992 cht3 27216 bclbnd 27324 bpos1lem 27326 bposlem4 27331 bposlem5 27332 bposlem8 27335 2lgslem3a 27440 2lgsoddprmlem3c 27456 2lgsoddprmlem3d 27457 ex-exp 30469 ex-fac 30470 ex-prmo 30478 ipasslem10 30858 siii 30872 normlem3 31131 bcsiALT 31198 dpmul1000 32881 hgt750lem2 34667 12lcm5e60 42009 60lcm7e420 42011 420lcm8e840 42012 3exp7 42054 3lexlogpow5ineq1 42055 3lexlogpow2ineq2 42060 3lexlogpow5ineq5 42061 aks4d1p1 42077 4t5e20 42326 235t711 42339 ex-decpmul 42340 0tie0 42350 3cubeslem3l 42697 3cubeslem3r 42698 sqrtcval2 43655 resqrtvalex 43658 inductionexd 44168 fouriersw 46246 1t10e1p1e11 47322 fmtno5lem1 47540 fmtno5lem2 47541 257prm 47548 fmtno4prmfac 47559 fmtno4nprmfac193 47561 fmtno5faclem2 47567 139prmALT 47583 127prm 47586 mod42tp1mod8 47589 3exp4mod41 47603 41prothprmlem2 47605 2exp340mod341 47720 8exp8mod9 47723 gpg5order 48014 |
| Copyright terms: Public domain | W3C validator |