![]() |
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 11219 | . 2 ⊢ (𝐵 · 𝐴) = (𝐴 · 𝐵) |
4 | mulcomli.3 | . 2 ⊢ (𝐴 · 𝐵) = 𝐶 | |
5 | 3, 4 | eqtri 2752 | 1 ⊢ (𝐵 · 𝐴) = 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 ∈ wcel 2098 (class class class)co 7401 ℂcc 11104 · cmul 11111 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-9 2108 ax-ext 2695 ax-mulcom 11170 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1774 df-cleq 2716 |
This theorem is referenced by: divcan1i 11955 mvllmuli 12044 recgt0ii 12117 nummul2c 12724 halfthird 12817 5recm6rec 12818 sq4e2t8 14160 cos2bnd 16128 prmo3 16973 dec5nprm 16998 decexp2 17007 karatsuba 17016 2exp6 17019 2exp8 17021 2exp11 17022 2exp16 17023 7prm 17043 13prm 17048 17prm 17049 19prm 17050 23prm 17051 43prm 17054 83prm 17055 139prm 17056 163prm 17057 317prm 17058 631prm 17059 1259lem1 17063 1259lem2 17064 1259lem3 17065 1259lem4 17066 1259lem5 17067 1259prm 17068 2503lem1 17069 2503lem2 17070 2503lem3 17071 2503prm 17072 4001lem1 17073 4001lem2 17074 4001lem3 17075 4001lem4 17076 4001prm 17077 pcoass 24873 efif1olem2 26394 mcubic 26695 quart1lem 26703 quart1 26704 quartlem1 26705 tanatan 26767 log2ublem3 26796 log2ub 26797 cht3 27021 bclbnd 27129 bpos1lem 27131 bposlem4 27136 bposlem5 27137 bposlem8 27140 2lgslem3a 27245 2lgsoddprmlem3c 27261 2lgsoddprmlem3d 27262 ex-exp 30172 ex-fac 30173 ex-prmo 30181 ipasslem10 30561 siii 30575 normlem3 30834 bcsiALT 30901 dpmul1000 32532 hgt750lem2 34153 12lcm5e60 41366 60lcm7e420 41368 420lcm8e840 41369 3exp7 41411 3lexlogpow5ineq1 41412 3lexlogpow2ineq2 41417 3lexlogpow5ineq5 41418 aks4d1p1 41434 4t5e20 41692 235t711 41694 ex-decpmul 41695 3cubeslem3l 41913 3cubeslem3r 41914 sqrtcval2 42882 resqrtvalex 42885 inductionexd 43395 fouriersw 45432 1t10e1p1e11 46503 fmtno5lem1 46706 fmtno5lem2 46707 257prm 46714 fmtno4prmfac 46725 fmtno4nprmfac193 46727 fmtno5faclem2 46733 139prmALT 46749 127prm 46752 mod42tp1mod8 46755 3exp4mod41 46769 41prothprmlem2 46771 2exp340mod341 46886 8exp8mod9 46889 |
Copyright terms: Public domain | W3C validator |