Theorem mulcomi 11187

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

Syntax hints:   = wceq 1559   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068   · cmul 11075

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

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

This theorem is referenced by:  mulcomli  11188  divmul13i  11949  8th4div3  12438  numma2c  12736  nummul2c  12740  9t11e99OLD  12821  binom2i  14222  fac3  14290  tanval2  16148  pockthi  16926  mod2xnegi  17090  decsplit1  17100  decsplit  17101  83prm  17142  dvsincos  26023  sincosq4sgn  26543  2logb9irrALT  26840  ang180lem3  26853  mcubic  26889  cubic2  26890  log2ublem2  26989  log2ublem3  26990  log2ub  26991  basellem8  27129  ppiub  27245  chtub  27253  bposlem8  27332  2lgsoddprmlem2  27450  2lgsoddprmlem3d  27454  ax5seglem7  29082  ex-ind-dvds  30609  ipdirilem  30978  siilem1  31000  bcseqi  31269  h1de2i  31702  dpmul10  33033  dpmul4  33052  signswch  34819  hgt750lem  34909  hgt750lem2  34910  problem4  35982  problem5  35983  quad3  35984  mulcomnni  42568  lcmineqlem23  42632  3lexlogpow5ineq1  42635  arearect  43756  areaquad  43757  wallispilem4  46606  dirkercncflem1  46641  fourierswlem  46768  goldratmolem2  47444  257prm  48134  fmtno4prmfac  48145  5tcu2e40  48188  41prothprm  48192  tgoldbachlt  48402  zlmodzxzequap  49085