Theorem mulcomi 11144

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027   · cmul 11034

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

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

This theorem is referenced by:  mulcomli  11145  divmul13i  11907  8th4div3  12388  numma2c  12681  nummul2c  12685  9t11e99  12765  binom2i  14165  fac3  14233  tanval2  16091  pockthi  16869  mod2xnegi  17033  decsplit1  17043  decsplit  17044  83prm  17084  dvsincos  25958  sincosq4sgn  26478  2logb9irrALT  26775  ang180lem3  26788  mcubic  26824  cubic2  26825  log2ublem2  26924  log2ublem3  26925  log2ub  26926  basellem8  27065  ppiub  27181  chtub  27189  bposlem8  27268  2lgsoddprmlem2  27386  2lgsoddprmlem3d  27390  ax5seglem7  29018  ex-ind-dvds  30546  ipdirilem  30915  siilem1  30937  bcseqi  31206  h1de2i  31639  dpmul10  32969  dpmul4  32988  signswch  34721  hgt750lem  34811  hgt750lem2  34812  problem4  35866  problem5  35867  quad3  35868  mulcomnni  42440  lcmineqlem23  42504  3lexlogpow5ineq1  42507  arearect  43661  areaquad  43662  wallispilem4  46514  dirkercncflem1  46549  fourierswlem  46676  257prm  48036  fmtno4prmfac  48047  5tcu2e40  48090  41prothprm  48094  tgoldbachlt  48304  zlmodzxzequap  48987