| 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 11241 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | |
| 4 | 1, 2, 3 | mp2an 692 | 1 ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∈ wcel 2108 (class class class)co 7431 ℂcc 11153 · cmul 11160 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-mulcom 11219 |
| This theorem depends on definitions: df-bi 207 df-an 396 |
| This theorem is referenced by: mulcomli 11270 divmul13i 12028 8th4div3 12486 numma2c 12779 nummul2c 12783 9t11e99 12863 binom2i 14251 fac3 14319 tanval2 16169 pockthi 16945 mod2xnegi 17109 decsplit1 17119 decsplit 17120 83prm 17160 dvsincos 26019 sincosq4sgn 26543 2logb9irrALT 26841 ang180lem3 26854 mcubic 26890 cubic2 26891 log2ublem2 26990 log2ublem3 26991 log2ub 26992 basellem8 27131 ppiub 27248 chtub 27256 bposlem8 27335 2lgsoddprmlem2 27453 2lgsoddprmlem3d 27457 ax5seglem7 28950 ex-ind-dvds 30480 ipdirilem 30848 siilem1 30870 bcseqi 31139 h1de2i 31572 dpmul10 32877 dpmul4 32896 signswch 34576 hgt750lem 34666 hgt750lem2 34667 problem4 35673 problem5 35674 quad3 35675 mulcomnni 41988 lcmineqlem23 42052 3lexlogpow5ineq1 42055 arearect 43227 areaquad 43228 wallispilem4 46083 dirkercncflem1 46118 fourierswlem 46245 257prm 47548 fmtno4prmfac 47559 5tcu2e40 47602 41prothprm 47606 tgoldbachlt 47803 zlmodzxzequap 48416 |
| Copyright terms: Public domain | W3C validator |