Theorem mulcomi 10643

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

Syntax hints:   = wceq 1533   ∈ wcel 2110  (class class class)co 7150  ℂcc 10529   · cmul 10536

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

This theorem depends on definitions:  df-bi 209  df-an 399

This theorem is referenced by:  mulcomli  10644  divmul13i  11395  8th4div3  11851  numma2c  12138  nummul2c  12142  9t11e99  12222  binom2i  13568  fac3  13634  tanval2  15480  pockthi  16237  mod2xnegi  16401  decexp2  16405  decsplit1  16412  decsplit  16413  83prm  16450  dvsincos  24572  sincosq4sgn  25081  2logb9irrALT  25370  ang180lem3  25383  mcubic  25419  cubic2  25420  log2ublem2  25519  log2ublem3  25520  log2ub  25521  basellem8  25659  ppiub  25774  chtub  25782  bposlem8  25861  2lgsoddprmlem2  25979  2lgsoddprmlem3d  25983  ax5seglem7  26715  ex-ind-dvds  28234  ipdirilem  28600  siilem1  28622  bcseqi  28891  h1de2i  29324  dpmul10  30566  dpmul4  30585  signswch  31826  hgt750lem  31917  hgt750lem2  31918  problem4  32906  problem5  32907  quad3  32908  arearect  39815  areaquad  39816  wallispilem4  42347  dirkercncflem1  42382  fourierswlem  42509  257prm  43717  fmtno4prmfac  43728  5tcu2e40  43774  41prothprm  43778  tgoldbachlt  43975  zlmodzxzequap  44548