Theorem mulcomi 11226

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

Syntax hints:   = wceq 1539   ∈ wcel 2104  (class class class)co 7411  ℂcc 11110   · cmul 11117

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

This theorem depends on definitions:  df-bi 206  df-an 395

This theorem is referenced by:  mulcomli  11227  divmul13i  11979  8th4div3  12436  numma2c  12727  nummul2c  12731  9t11e99  12811  binom2i  14180  fac3  14244  tanval2  16080  pockthi  16844  mod2xnegi  17008  decexp2  17012  decsplit1  17019  decsplit  17020  83prm  17060  dvsincos  25733  sincosq4sgn  26247  2logb9irrALT  26539  ang180lem3  26552  mcubic  26588  cubic2  26589  log2ublem2  26688  log2ublem3  26689  log2ub  26690  basellem8  26828  ppiub  26943  chtub  26951  bposlem8  27030  2lgsoddprmlem2  27148  2lgsoddprmlem3d  27152  ax5seglem7  28460  ex-ind-dvds  29981  ipdirilem  30349  siilem1  30371  bcseqi  30640  h1de2i  31073  dpmul10  32328  dpmul4  32347  signswch  33870  hgt750lem  33961  hgt750lem2  33962  problem4  34951  problem5  34952  quad3  34953  mulcomnni  41159  lcmineqlem23  41222  3lexlogpow5ineq1  41225  arearect  42266  areaquad  42267  wallispilem4  45082  dirkercncflem1  45117  fourierswlem  45244  257prm  46527  fmtno4prmfac  46538  5tcu2e40  46581  41prothprm  46585  tgoldbachlt  46782  zlmodzxzequap  47267