Theorem mulcomi 10638

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

Syntax hints:   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524   · cmul 10531

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

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

This theorem is referenced by:  mulcomli  10639  divmul13i  11390  8th4div3  11845  numma2c  12132  nummul2c  12136  9t11e99  12216  binom2i  13570  fac3  13636  tanval2  15478  pockthi  16233  mod2xnegi  16397  decexp2  16401  decsplit1  16408  decsplit  16409  83prm  16448  dvsincos  24584  sincosq4sgn  25094  2logb9irrALT  25384  ang180lem3  25397  mcubic  25433  cubic2  25434  log2ublem2  25533  log2ublem3  25534  log2ub  25535  basellem8  25673  ppiub  25788  chtub  25796  bposlem8  25875  2lgsoddprmlem2  25993  2lgsoddprmlem3d  25997  ax5seglem7  26729  ex-ind-dvds  28246  ipdirilem  28612  siilem1  28634  bcseqi  28903  h1de2i  29336  dpmul10  30597  dpmul4  30616  signswch  31941  hgt750lem  32032  hgt750lem2  32033  problem4  33024  problem5  33025  quad3  33026  mulcomnni  39275  lcmineqlem23  39339  3lexlogpow5ineq1  39341  arearect  40165  areaquad  40166  wallispilem4  42710  dirkercncflem1  42745  fourierswlem  42872  257prm  44078  fmtno4prmfac  44089  5tcu2e40  44133  41prothprm  44137  tgoldbachlt  44334  zlmodzxzequap  44908