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 10611 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | |
4 | 1, 2, 3 | mp2an 688 | 1 ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ∈ wcel 2105 (class class class)co 7145 ℂcc 10523 · cmul 10530 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-mulcom 10589 |
This theorem depends on definitions: df-bi 208 df-an 397 |
This theorem is referenced by: mulcomli 10638 divmul13i 11389 8th4div3 11845 numma2c 12132 nummul2c 12136 9t11e99 12216 binom2i 13562 fac3 13628 tanval2 15474 pockthi 16231 mod2xnegi 16395 decexp2 16399 decsplit1 16406 decsplit 16407 83prm 16444 dvsincos 24505 sincosq4sgn 25014 2logb9irrALT 25303 ang180lem3 25316 mcubic 25352 cubic2 25353 log2ublem2 25452 log2ublem3 25453 log2ub 25454 basellem8 25592 ppiub 25707 chtub 25715 bposlem8 25794 2lgsoddprmlem2 25912 2lgsoddprmlem3d 25916 ax5seglem7 26648 ex-ind-dvds 28167 ipdirilem 28533 siilem1 28555 bcseqi 28824 h1de2i 29257 dpmul10 30498 dpmul4 30517 signswch 31730 hgt750lem 31821 hgt750lem2 31822 problem4 32808 problem5 32809 quad3 32810 arearect 39700 areaquad 39701 wallispilem4 42230 dirkercncflem1 42265 fourierswlem 42392 257prm 43600 fmtno4prmfac 43611 5tcu2e40 43657 41prothprm 43661 tgoldbachlt 43858 zlmodzxzequap 44482 |
Copyright terms: Public domain | W3C validator |