Theorem mulcomi 10889

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

Syntax hints:   = wceq 1543   ∈ wcel 2112  (class class class)co 7252  ℂcc 10775   · cmul 10782

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

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

This theorem is referenced by:  mulcomli  10890  divmul13i  11641  8th4div3  12098  numma2c  12387  nummul2c  12391  9t11e99  12471  binom2i  13831  fac3  13897  tanval2  15745  pockthi  16511  mod2xnegi  16675  decexp2  16679  decsplit1  16686  decsplit  16687  83prm  16727  dvsincos  25025  sincosq4sgn  25538  2logb9irrALT  25828  ang180lem3  25841  mcubic  25877  cubic2  25878  log2ublem2  25977  log2ublem3  25978  log2ub  25979  basellem8  26117  ppiub  26232  chtub  26240  bposlem8  26319  2lgsoddprmlem2  26437  2lgsoddprmlem3d  26441  ax5seglem7  27181  ex-ind-dvds  28701  ipdirilem  29067  siilem1  29089  bcseqi  29358  h1de2i  29791  dpmul10  31046  dpmul4  31065  signswch  32415  hgt750lem  32506  hgt750lem2  32507  problem4  33501  problem5  33502  quad3  33503  mulcomnni  39903  lcmineqlem23  39966  3lexlogpow5ineq1  39969  arearect  40934  areaquad  40935  wallispilem4  43472  dirkercncflem1  43507  fourierswlem  43634  257prm  44874  fmtno4prmfac  44885  5tcu2e40  44928  41prothprm  44932  tgoldbachlt  45129  zlmodzxzequap  45701