Theorem mulcomi 11152

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   · cmul 11043

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

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

This theorem is referenced by:  mulcomli  11153  divmul13i  11914  8th4div3  12373  numma2c  12665  nummul2c  12669  9t11e99  12749  binom2i  14147  fac3  14215  tanval2  16070  pockthi  16847  mod2xnegi  17011  decsplit1  17021  decsplit  17022  83prm  17062  dvsincos  25953  sincosq4sgn  26478  2logb9irrALT  26776  ang180lem3  26789  mcubic  26825  cubic2  26826  log2ublem2  26925  log2ublem3  26926  log2ub  26927  basellem8  27066  ppiub  27183  chtub  27191  bposlem8  27270  2lgsoddprmlem2  27388  2lgsoddprmlem3d  27392  ax5seglem7  29020  ex-ind-dvds  30548  ipdirilem  30916  siilem1  30938  bcseqi  31207  h1de2i  31640  dpmul10  32986  dpmul4  33005  signswch  34738  hgt750lem  34828  hgt750lem2  34829  problem4  35881  problem5  35882  quad3  35883  mulcomnni  42351  lcmineqlem23  42415  3lexlogpow5ineq1  42418  arearect  43566  areaquad  43567  wallispilem4  46420  dirkercncflem1  46455  fourierswlem  46582  257prm  47915  fmtno4prmfac  47926  5tcu2e40  47969  41prothprm  47973  tgoldbachlt  48170  zlmodzxzequap  48853