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 10022 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | |
4 | 1, 2, 3 | mp2an 708 | 1 ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1483 ∈ wcel 1990 (class class class)co 6650 ℂcc 9934 · cmul 9941 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-mulcom 10000 |
This theorem depends on definitions: df-bi 197 df-an 386 |
This theorem is referenced by: mulcomli 10047 divmul13i 10786 8th4div3 11252 numma2c 11559 nummul2c 11563 9t11e99 11671 9t11e99OLD 11672 binom2i 12974 fac3 13067 tanval2 14863 pockthi 15611 mod2xnegi 15775 decexp2 15779 decsplit1 15786 decsplit 15787 decsplit1OLD 15790 decsplitOLD 15791 83prm 15830 dvsincos 23744 sincosq4sgn 24253 ang180lem3 24541 mcubic 24574 cubic2 24575 log2ublem2 24674 log2ublem3 24675 log2ub 24676 basellem8 24814 ppiub 24929 chtub 24937 bposlem8 25016 2lgsoddprmlem2 25134 2lgsoddprmlem3d 25138 ax5seglem7 25815 ex-exp 27307 ex-ind-dvds 27318 ipdirilem 27684 siilem1 27706 bcseqi 27977 h1de2i 28412 dpmul10 29603 dpmul4 29622 signswch 30638 hgt750lem 30729 hgt750lem2 30730 problem4 31562 problem5 31563 quad3 31564 arearect 37801 areaquad 37802 wallispilem4 40285 dirkercncflem1 40320 fourierswlem 40447 257prm 41473 fmtno4prmfac 41484 5tcu2e40 41532 41prothprm 41536 tgoldbachlt 41704 tgoldbachltOLD 41710 zlmodzxzequap 42288 |
Copyright terms: Public domain | W3C validator |