Theorem mulcomi 11140

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   · cmul 11031

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

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

This theorem is referenced by:  mulcomli  11141  divmul13i  11902  8th4div3  12361  numma2c  12653  nummul2c  12657  9t11e99  12737  binom2i  14135  fac3  14203  tanval2  16058  pockthi  16835  mod2xnegi  16999  decsplit1  17009  decsplit  17010  83prm  17050  dvsincos  25941  sincosq4sgn  26466  2logb9irrALT  26764  ang180lem3  26777  mcubic  26813  cubic2  26814  log2ublem2  26913  log2ublem3  26914  log2ub  26915  basellem8  27054  ppiub  27171  chtub  27179  bposlem8  27258  2lgsoddprmlem2  27376  2lgsoddprmlem3d  27380  ax5seglem7  29008  ex-ind-dvds  30536  ipdirilem  30904  siilem1  30926  bcseqi  31195  h1de2i  31628  dpmul10  32976  dpmul4  32995  signswch  34718  hgt750lem  34808  hgt750lem2  34809  problem4  35862  problem5  35863  quad3  35864  mulcomnni  42237  lcmineqlem23  42301  3lexlogpow5ineq1  42304  arearect  43453  areaquad  43454  wallispilem4  46308  dirkercncflem1  46343  fourierswlem  46470  257prm  47803  fmtno4prmfac  47814  5tcu2e40  47857  41prothprm  47861  tgoldbachlt  48058  zlmodzxzequap  48741