Theorem mulcomi 11298

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  (class class class)co 7412  ℂcc 11179   · cmul 11186

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

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

This theorem is used by:  mulcomli  11299  divmul13i  12059  8th4div3  12547  numma2c  12846  nummul2c  12850  9t11e99OLD  12931  binom2i  14336  tanval2  16281  pockthi  17065  mod2xnegi  17229  decsplit1  17239  decsplit  17240  83prm  17281  dvsincos  26281  sincosq4sgn  26812  2logb9irrALT  27108  ang180lem3  27121  mcubic  27157  cubic2  27158  log2ublem2  27257  log2ublem3  27258  log2ub  27259  chtub  27521  bposlem8  27600  2lgsoddprmlem2  27718  2lgsoddprmlem3d  27722  ax5seglem7  29495  ex-ind-dvds  31044  ipdirilem  31413  siilem1  31435  bcseqi  31704  h1de2i  32137  dpmul10  33443  dpmul4  33462  signswch  35173  hgt750lem  35263  hgt750lem2  35264  problem4  36402  problem5  36403  quad3  36404  mulcomnni  43005  lcmineqlem23  43069  3lexlogpow5ineq1  43072  arearect  44175  areaquad  44176  wallispilem4  47022  dirkercncflem1  47057  fourierswlem  47184  goldpolyfactor  47871  goldratmolem2  47877  257prm  48590  fmtno4prmfac  48601  5tcu2e40  48644  41prothprm  48648  tgoldbachlt  48858  zlmodzxzequap  49555