Theorem mulcomi 11189

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073   · cmul 11080

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

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

This theorem is referenced by:  mulcomli  11190  divmul13i  11950  8th4div3  12409  numma2c  12702  nummul2c  12706  9t11e99  12786  binom2i  14184  fac3  14252  tanval2  16108  pockthi  16885  mod2xnegi  17049  decsplit1  17059  decsplit  17060  83prm  17100  dvsincos  25892  sincosq4sgn  26417  2logb9irrALT  26715  ang180lem3  26728  mcubic  26764  cubic2  26765  log2ublem2  26864  log2ublem3  26865  log2ub  26866  basellem8  27005  ppiub  27122  chtub  27130  bposlem8  27209  2lgsoddprmlem2  27327  2lgsoddprmlem3d  27331  ax5seglem7  28869  ex-ind-dvds  30397  ipdirilem  30765  siilem1  30787  bcseqi  31056  h1de2i  31489  dpmul10  32822  dpmul4  32841  signswch  34559  hgt750lem  34649  hgt750lem2  34650  problem4  35662  problem5  35663  quad3  35664  mulcomnni  41982  lcmineqlem23  42046  3lexlogpow5ineq1  42049  arearect  43211  areaquad  43212  wallispilem4  46073  dirkercncflem1  46108  fourierswlem  46235  257prm  47566  fmtno4prmfac  47577  5tcu2e40  47620  41prothprm  47624  tgoldbachlt  47821  zlmodzxzequap  48492