Theorem mulcomi 11218

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

Syntax hints:   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099   · cmul 11106

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

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

This theorem is referenced by:  mulcomli  11219  divmul13i  11977  8th4div3  12465  numma2c  12763  nummul2c  12767  9t11e99OLD  12848  binom2i  14250  tanval2  16190  pockthi  16968  mod2xnegi  17132  decsplit1  17142  decsplit  17143  83prm  17184  dvsincos  26121  sincosq4sgn  26644  2logb9irrALT  26941  ang180lem3  26954  mcubic  26990  cubic2  26991  log2ublem2  27090  log2ublem3  27091  log2ub  27092  basellem8  27230  ppiub  27346  chtub  27354  bposlem8  27433  2lgsoddprmlem2  27551  2lgsoddprmlem3d  27555  ax5seglem7  29263  ex-ind-dvds  30790  ipdirilem  31159  siilem1  31181  bcseqi  31450  h1de2i  31883  dpmul10  33192  dpmul4  33211  signswch  34926  hgt750lem  35016  hgt750lem2  35017  problem4  36138  problem5  36139  quad3  36140  mulcomnni  42732  lcmineqlem23  42796  3lexlogpow5ineq1  42799  arearect  43922  areaquad  43923  wallispilem4  46762  dirkercncflem1  46797  fourierswlem  46924  goldratmolem2  47600  257prm  48290  fmtno4prmfac  48301  5tcu2e40  48344  41prothprm  48348  tgoldbachlt  48558  zlmodzxzequap  49256