Theorem mulcomi 11117

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

Syntax hints:   = wceq 1541   ∈ wcel 2111  (class class class)co 7346  ℂcc 11001   · cmul 11008

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

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

This theorem is referenced by:  mulcomli  11118  divmul13i  11879  8th4div3  12338  numma2c  12631  nummul2c  12635  9t11e99  12715  binom2i  14116  fac3  14184  tanval2  16039  pockthi  16816  mod2xnegi  16980  decsplit1  16990  decsplit  16991  83prm  17031  dvsincos  25910  sincosq4sgn  26435  2logb9irrALT  26733  ang180lem3  26746  mcubic  26782  cubic2  26783  log2ublem2  26882  log2ublem3  26883  log2ub  26884  basellem8  27023  ppiub  27140  chtub  27148  bposlem8  27227  2lgsoddprmlem2  27345  2lgsoddprmlem3d  27349  ax5seglem7  28911  ex-ind-dvds  30436  ipdirilem  30804  siilem1  30826  bcseqi  31095  h1de2i  31528  dpmul10  32870  dpmul4  32889  signswch  34569  hgt750lem  34659  hgt750lem2  34660  problem4  35700  problem5  35701  quad3  35702  mulcomnni  42019  lcmineqlem23  42083  3lexlogpow5ineq1  42086  arearect  43247  areaquad  43248  wallispilem4  46105  dirkercncflem1  46140  fourierswlem  46267  257prm  47591  fmtno4prmfac  47602  5tcu2e40  47645  41prothprm  47649  tgoldbachlt  47846  zlmodzxzequap  48530