Theorem mulcomi 11245

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  (class class class)co 7417  ℂcc 11126   · cmul 11133

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 11192

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mulcomli  11246  divmul13i  12004  8th4div3  12492  numma2c  12791  nummul2c  12795  9t11e99OLD  12876  binom2i  14280  tanval2  16227  pockthi  17005  mod2xnegi  17169  decsplit1  17179  decsplit  17180  83prm  17221  dvsincos  26215  sincosq4sgn  26746  2logb9irrALT  27043  ang180lem3  27056  mcubic  27092  cubic2  27093  log2ublem2  27192  log2ublem3  27193  log2ub  27194  chtub  27456  bposlem8  27535  2lgsoddprmlem2  27653  2lgsoddprmlem3d  27657  ax5seglem7  29400  ex-ind-dvds  30949  ipdirilem  31318  siilem1  31340  bcseqi  31609  h1de2i  32042  dpmul10  33348  dpmul4  33367  signswch  35077  hgt750lem  35167  hgt750lem2  35168  problem4  36255  problem5  36256  quad3  36257  mulcomnni  42861  lcmineqlem23  42925  3lexlogpow5ineq1  42928  arearect  44064  areaquad  44065  wallispilem4  46904  dirkercncflem1  46939  fourierswlem  47066  goldpolyfactor  47753  goldratmolem2  47759  257prm  48472  fmtno4prmfac  48483  5tcu2e40  48526  41prothprm  48530  tgoldbachlt  48740  zlmodzxzequap  49437