Theorem mulcomi 11269

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153   · cmul 11160

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

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

This theorem is referenced by:  mulcomli  11270  divmul13i  12028  8th4div3  12486  numma2c  12779  nummul2c  12783  9t11e99  12863  binom2i  14251  fac3  14319  tanval2  16169  pockthi  16945  mod2xnegi  17109  decsplit1  17119  decsplit  17120  83prm  17160  dvsincos  26019  sincosq4sgn  26543  2logb9irrALT  26841  ang180lem3  26854  mcubic  26890  cubic2  26891  log2ublem2  26990  log2ublem3  26991  log2ub  26992  basellem8  27131  ppiub  27248  chtub  27256  bposlem8  27335  2lgsoddprmlem2  27453  2lgsoddprmlem3d  27457  ax5seglem7  28950  ex-ind-dvds  30480  ipdirilem  30848  siilem1  30870  bcseqi  31139  h1de2i  31572  dpmul10  32877  dpmul4  32896  signswch  34576  hgt750lem  34666  hgt750lem2  34667  problem4  35673  problem5  35674  quad3  35675  mulcomnni  41988  lcmineqlem23  42052  3lexlogpow5ineq1  42055  arearect  43227  areaquad  43228  wallispilem4  46083  dirkercncflem1  46118  fourierswlem  46245  257prm  47548  fmtno4prmfac  47559  5tcu2e40  47602  41prothprm  47606  tgoldbachlt  47803  zlmodzxzequap  48416