Theorem mulcomi 9925

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

Syntax hints:   = wceq 1475   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   · cmul 9820

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

This theorem depends on definitions:  df-bi 196  df-an 385

This theorem is referenced by:  mulcomli  9926  divmul13i  10665  8th4div3  11129  numma2c  11435  nummul2c  11439  9t11e99  11547  9t11e99OLD  11548  binom2i  12836  fac3  12929  tanval2  14702  pockthi  15449  mod2xnegi  15613  decexp2  15617  decsplit1  15624  decsplit  15625  decsplit1OLD  15628  decsplitOLD  15629  83prm  15668  dvsincos  23548  sincosq4sgn  24057  ang180lem3  24341  mcubic  24374  cubic2  24375  log2ublem2  24474  log2ublem3  24475  log2ub  24476  basellem8  24614  ppiub  24729  chtub  24737  bposlem8  24816  2lgsoddprmlem2  24934  2lgsoddprmlem3d  24938  ax5seglem7  25615  ex-exp  26699  ex-ind-dvds  26710  ipdirilem  27068  siilem1  27090  bcseqi  27361  h1de2i  27796  signswch  29964  problem4  30816  problem5  30817  quad3  30818  arearect  36820  areaquad  36821  wallispilem4  38961  dirkercncflem1  38996  fourierswlem  39123  257prm  40011  fmtno4prmfac  40022  5tcu2e40  40070  41prothprm  40074  tgoldbachlt  40230  tgoldbachltOLD  40237  zlmodzxzequap  42082