Theorem mulcomi 11151

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

Syntax hints:   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034   · cmul 11041

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

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  mulcomli  11152  divmul13i  11914  8th4div3  12395  numma2c  12688  nummul2c  12692  9t11e99  12772  binom2i  14172  fac3  14240  tanval2  16098  pockthi  16876  mod2xnegi  17040  decsplit1  17050  decsplit  17051  83prm  17091  dvsincos  25973  sincosq4sgn  26490  2logb9irrALT  26787  ang180lem3  26800  mcubic  26836  cubic2  26837  log2ublem2  26936  log2ublem3  26937  log2ub  26938  basellem8  27076  ppiub  27192  chtub  27200  bposlem8  27279  2lgsoddprmlem2  27397  2lgsoddprmlem3d  27401  ax5seglem7  29029  ex-ind-dvds  30556  ipdirilem  30925  siilem1  30947  bcseqi  31216  h1de2i  31649  dpmul10  32980  dpmul4  32999  signswch  34752  hgt750lem  34842  hgt750lem2  34843  problem4  35903  problem5  35904  quad3  35905  mulcomnni  42479  lcmineqlem23  42543  3lexlogpow5ineq1  42546  arearect  43667  areaquad  43668  wallispilem4  46518  dirkercncflem1  46553  fourierswlem  46680  goldratmolem2  47356  257prm  48046  fmtno4prmfac  48057  5tcu2e40  48100  41prothprm  48104  tgoldbachlt  48314  zlmodzxzequap  48997