Theorem mulcomi 11153

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036   · cmul 11043

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

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  mulcomli  11154  divmul13i  11916  8th4div3  12397  numma2c  12690  nummul2c  12694  9t11e99  12774  binom2i  14174  fac3  14242  tanval2  16100  pockthi  16878  mod2xnegi  17042  decsplit1  17052  decsplit  17053  83prm  17093  dvsincos  25948  sincosq4sgn  26465  2logb9irrALT  26762  ang180lem3  26775  mcubic  26811  cubic2  26812  log2ublem2  26911  log2ublem3  26912  log2ub  26913  basellem8  27051  ppiub  27167  chtub  27175  bposlem8  27254  2lgsoddprmlem2  27372  2lgsoddprmlem3d  27376  ax5seglem7  29004  ex-ind-dvds  30531  ipdirilem  30900  siilem1  30922  bcseqi  31191  h1de2i  31624  dpmul10  32954  dpmul4  32973  signswch  34705  hgt750lem  34795  hgt750lem2  34796  problem4  35850  problem5  35851  quad3  35852  mulcomnni  42426  lcmineqlem23  42490  3lexlogpow5ineq1  42493  arearect  43643  areaquad  43644  wallispilem4  46496  dirkercncflem1  46531  fourierswlem  46658  goldratmolem2  47334  257prm  48024  fmtno4prmfac  48035  5tcu2e40  48078  41prothprm  48082  tgoldbachlt  48292  zlmodzxzequap  48975