Theorem mulcomi 10259

Description: Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ
axi.2	⊢ 𝐵 ∈ ℂ

Assertion

Ref	Expression
mulcomi	⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)

Proof of Theorem mulcomi

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		axi.2	. 2 ⊢ 𝐵 ∈ ℂ
3		mulcom 10235	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
4	1, 2, 3	mp2an 710	1 ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)

Syntax hints:   = wceq 1632   ∈ wcel 2140  (class class class)co 6815  ℂcc 10147   · cmul 10154

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 10213

This theorem depends on definitions:  df-bi 197  df-an 385

This theorem is referenced by:  mulcomli  10260  divmul13i  10999  8th4div3  11465  numma2c  11772  nummul2c  11776  9t11e99  11884  9t11e99OLD  11885  binom2i  13189  fac3  13282  tanval2  15083  pockthi  15834  mod2xnegi  15998  decexp2  16002  decsplit1  16009  decsplit  16010  decsplit1OLD  16013  decsplitOLD  16014  83prm  16053  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  27640  ex-ind-dvds  27651  ipdirilem  28015  siilem1  28037  bcseqi  28308  h1de2i  28743  dpmul10  29934  dpmul4  29953  signswch  30969  hgt750lem  31060  hgt750lem2  31061  problem4  31891  problem5  31892  quad3  31893  arearect  38322  areaquad  38323  wallispilem4  40807  dirkercncflem1  40842  fourierswlem  40969  257prm  42002  fmtno4prmfac  42013  5tcu2e40  42061  41prothprm  42065  tgoldbachlt  42233  tgoldbachltOLD  42239  zlmodzxzequap  42817