![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mulcomi | Structured version Visualization version GIF version |
Description: Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Ref | Expression |
---|---|
axi.1 | ⊢ 𝐴 ∈ ℂ |
axi.2 | ⊢ 𝐵 ∈ ℂ |
Ref | Expression |
---|---|
mulcomi | ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axi.1 | . 2 ⊢ 𝐴 ∈ ℂ | |
2 | axi.2 | . 2 ⊢ 𝐵 ∈ ℂ | |
3 | mulcom 10228 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | |
4 | 1, 2, 3 | mp2an 672 | 1 ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1631 ∈ wcel 2145 (class class class)co 6796 ℂcc 10140 · cmul 10147 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-mulcom 10206 |
This theorem depends on definitions: df-bi 197 df-an 383 |
This theorem is referenced by: mulcomli 10253 divmul13i 10992 8th4div3 11459 numma2c 11765 nummul2c 11769 9t11e99 11877 9t11e99OLD 11878 binom2i 13181 fac3 13271 tanval2 15069 pockthi 15818 mod2xnegi 15982 decexp2 15986 decsplit1 15993 decsplit 15994 decsplit1OLD 15997 decsplitOLD 15998 83prm 16037 dvsincos 23964 sincosq4sgn 24474 ang180lem3 24762 mcubic 24795 cubic2 24796 log2ublem2 24895 log2ublem3 24896 log2ub 24897 basellem8 25035 ppiub 25150 chtub 25158 bposlem8 25237 2lgsoddprmlem2 25355 2lgsoddprmlem3d 25359 ax5seglem7 26036 ex-exp 27649 ex-ind-dvds 27660 ipdirilem 28024 siilem1 28046 bcseqi 28317 h1de2i 28752 dpmul10 29943 dpmul4 29962 signswch 30978 hgt750lem 31069 hgt750lem2 31070 problem4 31900 problem5 31901 quad3 31902 arearect 38325 areaquad 38326 wallispilem4 40797 dirkercncflem1 40832 fourierswlem 40959 257prm 41996 fmtno4prmfac 42007 5tcu2e40 42055 41prothprm 42059 tgoldbachlt 42227 tgoldbachltOLD 42233 zlmodzxzequap 42811 |
Copyright terms: Public domain | W3C validator |