Theorem mulcomi 10728

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

Syntax hints:   = wceq 1542   ∈ wcel 2113  (class class class)co 7171  ℂcc 10614   · cmul 10621

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

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  mulcomli  10729  divmul13i  11480  8th4div3  11937  numma2c  12226  nummul2c  12230  9t11e99  12310  binom2i  13667  fac3  13733  tanval2  15579  pockthi  16344  mod2xnegi  16508  decexp2  16512  decsplit1  16519  decsplit  16520  83prm  16560  dvsincos  24733  sincosq4sgn  25246  2logb9irrALT  25536  ang180lem3  25549  mcubic  25585  cubic2  25586  log2ublem2  25685  log2ublem3  25686  log2ub  25687  basellem8  25825  ppiub  25940  chtub  25948  bposlem8  26027  2lgsoddprmlem2  26145  2lgsoddprmlem3d  26149  ax5seglem7  26881  ex-ind-dvds  28398  ipdirilem  28764  siilem1  28786  bcseqi  29055  h1de2i  29488  dpmul10  30744  dpmul4  30763  signswch  32110  hgt750lem  32201  hgt750lem2  32202  problem4  33197  problem5  33198  quad3  33199  mulcomnni  39613  lcmineqlem23  39676  3lexlogpow5ineq1  39679  arearect  40610  areaquad  40611  wallispilem4  43143  dirkercncflem1  43178  fourierswlem  43305  257prm  44539  fmtno4prmfac  44550  5tcu2e40  44593  41prothprm  44597  tgoldbachlt  44794  zlmodzxzequap  45366