![]() |
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 10258 | . 2 ⊢ (𝐵 · 𝐴) = (𝐴 · 𝐵) |
4 | mulcomli.3 | . 2 ⊢ (𝐴 · 𝐵) = 𝐶 | |
5 | 3, 4 | eqtri 2782 | 1 ⊢ (𝐵 · 𝐴) = 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1632 ∈ wcel 2139 (class class class)co 6814 ℂcc 10146 · cmul 10153 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-ext 2740 ax-mulcom 10212 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1854 df-cleq 2753 |
This theorem is referenced by: divcan1i 10981 mvllmuli 11070 recgt0ii 11141 nummul2c 11775 halfthird 11897 5recm6rec 11898 sq4e2t8 13176 cos2bnd 15137 prmo3 15967 dec5nprm 15992 decexp2 16001 karatsuba 16014 karatsubaOLD 16015 2exp6 16017 2exp8 16018 2exp16 16019 7prm 16039 13prm 16045 17prm 16046 19prm 16047 23prm 16048 43prm 16051 83prm 16052 139prm 16053 163prm 16054 317prm 16055 631prm 16056 1259lem1 16060 1259lem2 16061 1259lem3 16062 1259lem4 16063 1259lem5 16064 1259prm 16065 2503lem1 16066 2503lem2 16067 2503lem3 16068 2503prm 16069 4001lem1 16070 4001lem2 16071 4001lem3 16072 4001lem4 16073 4001prm 16074 pcoass 23044 efif1olem2 24509 mcubic 24794 quart1lem 24802 quart1 24803 quartlem1 24804 tanatan 24866 log2ublem3 24895 log2ub 24896 cht3 25119 bclbnd 25225 bpos1lem 25227 bposlem4 25232 bposlem5 25233 bposlem8 25236 2lgslem3a 25341 2lgsoddprmlem3c 25357 2lgsoddprmlem3d 25358 ex-fac 27640 ex-prmo 27648 ipasslem10 28024 siii 28038 normlem3 28299 bcsiALT 28366 dpmul1000 29937 hgt750lem2 31060 inductionexd 38973 fouriersw 40969 1t10e1p1e11 41847 1t10e1p1e11OLD 41848 fmtno5lem1 41993 fmtno5lem2 41994 257prm 42001 fmtno4prmfac 42012 fmtno4nprmfac193 42014 fmtno5faclem2 42020 139prmALT 42039 127prm 42043 2exp11 42045 mod42tp1mod8 42047 3exp4mod41 42061 41prothprmlem2 42063 |
Copyright terms: Public domain | W3C validator |