Theorem mulcomi 10337

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

Syntax hints:   = wceq 1653   ∈ wcel 2157  (class class class)co 6878  ℂcc 10222   · cmul 10229

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

This theorem depends on definitions:  df-bi 199  df-an 386

This theorem is referenced by:  mulcomli  10338  divmul13i  11078  8th4div3  11540  numma2c  11830  nummul2c  11834  9t11e99  11915  binom2i  13228  fac3  13320  tanval2  15199  pockthi  15944  mod2xnegi  16108  decexp2  16112  decsplit1  16119  decsplit  16120  83prm  16157  dvsincos  24085  sincosq4sgn  24595  2logb9irrALT  24880  ang180lem3  24893  mcubic  24926  cubic2  24927  log2ublem2  25026  log2ublem3  25027  log2ub  25028  basellem8  25166  ppiub  25281  chtub  25289  bposlem8  25368  2lgsoddprmlem2  25486  2lgsoddprmlem3d  25490  ax5seglem7  26172  ex-ind-dvds  27846  ipdirilem  28209  siilem1  28231  bcseqi  28502  h1de2i  28937  dpmul10  30119  dpmul4  30138  signswch  31156  hgt750lem  31249  hgt750lem2  31250  problem4  32077  problem5  32078  quad3  32079  arearect  38585  areaquad  38586  wallispilem4  41028  dirkercncflem1  41063  fourierswlem  41190  257prm  42255  fmtno4prmfac  42266  5tcu2e40  42314  41prothprm  42318  tgoldbachlt  42486  zlmodzxzequap  43087