Theorem mulassi 11208

Description: Associative law for multiplication. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ
axi.2	⊢ 𝐵 ∈ ℂ
axi.3	⊢ 𝐶 ∈ ℂ

Assertion

Ref	Expression
mulassi	⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))

Proof of Theorem mulassi

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		axi.2	. 2 ⊢ 𝐵 ∈ ℂ
3		axi.3	. 2 ⊢ 𝐶 ∈ ℂ
4		mulass 11176	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
5	1, 2, 3, 4	mp3an 1485	1 ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))

Syntax hints:   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086   · cmul 11093

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103

This theorem is referenced by:  8th4div3  12455  numma  12751  decbin0  12849  sq4e2t8  14226  3dec  14293  faclbnd4lem1  14320  ef01bndlem  16230  3dvdsdec  16380  3dvds2dec  16381  dec5dvds  17114  karatsuba  17133  sincos4thpi  26636  sincos6thpi  26639  ang180lem2  26933  ang180lem3  26934  asin1  27017  efiatan2  27040  2efiatan  27041  log2cnv  27067  log2ublem2  27070  log2ublem3  27071  log2ub  27072  bclbnd  27402  bposlem8  27413  2lgsoddprmlem3d  27535  ax5seglem7  29194  ipasslem10  31100  siilem1  31112  normlem0  31370  normlem9  31379  bcseqi  31381  polid2i  31418  dfdec100  33087  dpmul100  33129  dpmul1000  33131  dpexpp1  33140  dpmul4  33146  quad3  36033  iexpire  36098  mulassnni  42615  sn-1ticom  43056  sn-0tie0  43085  fourierswlem  46802  fouriersw  46803  cos5t  47471  goldratmolem2  47478  41prothprm  48226  tgoldbachlt  48436