Theorem mulcomi 11218

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

Syntax hints:   = wceq 1533   ∈ wcel 2098  (class class class)co 7401  ℂcc 11103   · cmul 11110

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

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

This theorem is referenced by:  mulcomli  11219  divmul13i  11971  8th4div3  12428  numma2c  12719  nummul2c  12723  9t11e99  12803  binom2i  14172  fac3  14236  tanval2  16072  pockthi  16838  mod2xnegi  17002  decexp2  17006  decsplit1  17013  decsplit  17014  83prm  17054  dvsincos  25834  sincosq4sgn  26352  2logb9irrALT  26645  ang180lem3  26658  mcubic  26694  cubic2  26695  log2ublem2  26794  log2ublem3  26795  log2ub  26796  basellem8  26935  ppiub  27052  chtub  27060  bposlem8  27139  2lgsoddprmlem2  27257  2lgsoddprmlem3d  27261  ax5seglem7  28628  ex-ind-dvds  30149  ipdirilem  30517  siilem1  30539  bcseqi  30808  h1de2i  31241  dpmul10  32494  dpmul4  32513  signswch  34027  hgt750lem  34118  hgt750lem2  34119  problem4  35108  problem5  35109  quad3  35110  mulcomnni  41312  lcmineqlem23  41375  3lexlogpow5ineq1  41378  arearect  42419  areaquad  42420  wallispilem4  45235  dirkercncflem1  45270  fourierswlem  45397  257prm  46680  fmtno4prmfac  46691  5tcu2e40  46734  41prothprm  46738  tgoldbachlt  46935  zlmodzxzequap  47334