Theorem mulassi 11238

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 11206	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
5	1, 2, 3, 4	mp3an 1490	1 ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116   · cmul 11123

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 11184

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  8th4div3  12482  numma  12778  decbin0  12876  sq4e2t8  14255  3dec  14322  faclbnd4lem1  14349  ef01bndlem  16265  3dvdsdec  16415  3dvds2dec  16416  dec5dvds  17149  karatsuba  17168  sincos4thpi  26715  sincos6thpi  26718  ang180lem2  27012  ang180lem3  27013  asin1  27096  efiatan2  27119  2efiatan  27120  log2cnv  27146  log2ublem2  27149  log2ublem3  27150  log2ub  27151  bclbnd  27481  bposlem8  27492  2lgsoddprmlem3d  27614  ax5seglem7  29322  ipasslem10  31228  siilem1  31240  normlem0  31498  normlem9  31507  bcseqi  31509  polid2i  31546  dfdec100  33211  dpmul100  33253  dpmul1000  33255  dpexpp1  33264  dpmul4  33270  quad3  36183  iexpire  36248  mulassnni  42794  sn-1ticom  43237  sn-0tie0  43266  fourierswlem  46985  fouriersw  46986  cos5t  47657  goldratmolem2  47664  41prothprm  48412  tgoldbachlt  48622  crosspdoti  50688  crossp3i  50690