Theorem mulcomi 11205

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 11174	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
4	1, 2, 3	mp2an 704	1 ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)

Syntax hints:   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086   · cmul 11093

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

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  mulcomli  11206  divmul13i  11967  8th4div3  12455  numma2c  12753  nummul2c  12757  9t11e99OLD  12838  binom2i  14239  fac3  14307  tanval2  16179  pockthi  16957  mod2xnegi  17121  decsplit1  17131  decsplit  17132  83prm  17173  dvsincos  26101  sincosq4sgn  26624  2logb9irrALT  26921  ang180lem3  26934  mcubic  26970  cubic2  26971  log2ublem2  27070  log2ublem3  27071  log2ub  27072  basellem8  27210  ppiub  27326  chtub  27334  bposlem8  27413  2lgsoddprmlem2  27531  2lgsoddprmlem3d  27535  ax5seglem7  29194  ex-ind-dvds  30721  ipdirilem  31090  siilem1  31112  bcseqi  31381  h1de2i  31814  dpmul10  33127  dpmul4  33146  signswch  34865  hgt750lem  34955  hgt750lem2  34956  problem4  36031  problem5  36032  quad3  36033  mulcomnni  42616  lcmineqlem23  42680  3lexlogpow5ineq1  42683  arearect  43804  areaquad  43805  wallispilem4  46640  dirkercncflem1  46675  fourierswlem  46802  goldratmolem2  47478  257prm  48168  fmtno4prmfac  48179  5tcu2e40  48222  41prothprm  48226  tgoldbachlt  48436  zlmodzxzequap  49130