Theorem mulcomi 11266

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

Syntax hints:   = wceq 1536   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150   · cmul 11157

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

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

This theorem is referenced by:  mulcomli  11267  divmul13i  12025  8th4div3  12483  numma2c  12776  nummul2c  12780  9t11e99  12860  binom2i  14247  fac3  14315  tanval2  16165  pockthi  16940  mod2xnegi  17104  decexp2  17108  decsplit1  17115  decsplit  17116  83prm  17156  dvsincos  26033  sincosq4sgn  26557  2logb9irrALT  26855  ang180lem3  26868  mcubic  26904  cubic2  26905  log2ublem2  27004  log2ublem3  27005  log2ub  27006  basellem8  27145  ppiub  27262  chtub  27270  bposlem8  27349  2lgsoddprmlem2  27467  2lgsoddprmlem3d  27471  ax5seglem7  28964  ex-ind-dvds  30489  ipdirilem  30857  siilem1  30879  bcseqi  31148  h1de2i  31581  dpmul10  32861  dpmul4  32880  signswch  34554  hgt750lem  34644  hgt750lem2  34645  problem4  35652  problem5  35653  quad3  35654  mulcomnni  41968  lcmineqlem23  42032  3lexlogpow5ineq1  42035  arearect  43203  areaquad  43204  wallispilem4  46023  dirkercncflem1  46058  fourierswlem  46185  257prm  47485  fmtno4prmfac  47496  5tcu2e40  47539  41prothprm  47543  tgoldbachlt  47740  zlmodzxzequap  48344