Theorem mulcomi 11142

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026   · cmul 11033

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

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

This theorem is referenced by:  mulcomli  11143  divmul13i  11903  8th4div3  12362  numma2c  12655  nummul2c  12659  9t11e99  12739  binom2i  14137  fac3  14205  tanval2  16060  pockthi  16837  mod2xnegi  17001  decsplit1  17011  decsplit  17012  83prm  17052  dvsincos  25901  sincosq4sgn  26426  2logb9irrALT  26724  ang180lem3  26737  mcubic  26773  cubic2  26774  log2ublem2  26873  log2ublem3  26874  log2ub  26875  basellem8  27014  ppiub  27131  chtub  27139  bposlem8  27218  2lgsoddprmlem2  27336  2lgsoddprmlem3d  27340  ax5seglem7  28898  ex-ind-dvds  30423  ipdirilem  30791  siilem1  30813  bcseqi  31082  h1de2i  31515  dpmul10  32848  dpmul4  32867  signswch  34528  hgt750lem  34618  hgt750lem2  34619  problem4  35640  problem5  35641  quad3  35642  mulcomnni  41960  lcmineqlem23  42024  3lexlogpow5ineq1  42027  arearect  43188  areaquad  43189  wallispilem4  46050  dirkercncflem1  46085  fourierswlem  46212  257prm  47546  fmtno4prmfac  47557  5tcu2e40  47600  41prothprm  47604  tgoldbachlt  47801  zlmodzxzequap  48485