Theorem mulcomi 11127

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011   · cmul 11018

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

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

This theorem is referenced by:  mulcomli  11128  divmul13i  11889  8th4div3  12348  numma2c  12640  nummul2c  12644  9t11e99  12724  binom2i  14121  fac3  14189  tanval2  16044  pockthi  16821  mod2xnegi  16985  decsplit1  16995  decsplit  16996  83prm  17036  dvsincos  25913  sincosq4sgn  26438  2logb9irrALT  26736  ang180lem3  26749  mcubic  26785  cubic2  26786  log2ublem2  26885  log2ublem3  26886  log2ub  26887  basellem8  27026  ppiub  27143  chtub  27151  bposlem8  27230  2lgsoddprmlem2  27348  2lgsoddprmlem3d  27352  ax5seglem7  28915  ex-ind-dvds  30443  ipdirilem  30811  siilem1  30833  bcseqi  31102  h1de2i  31535  dpmul10  32882  dpmul4  32901  signswch  34595  hgt750lem  34685  hgt750lem2  34686  problem4  35733  problem5  35734  quad3  35735  mulcomnni  42100  lcmineqlem23  42164  3lexlogpow5ineq1  42167  arearect  43332  areaquad  43333  wallispilem4  46190  dirkercncflem1  46225  fourierswlem  46352  257prm  47685  fmtno4prmfac  47696  5tcu2e40  47739  41prothprm  47743  tgoldbachlt  47940  zlmodzxzequap  48624