Theorem mulassi 11323

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201   · cmul 11208

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

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

This theorem is used by:  8th4div3  12569  numma  12866  decbin0  12964  sq4e2t8  14345  3dec  14413  faclbnd4lem1  14440  ef01bndlem  16357  3dvdsdec  16507  3dvds2dec  16508  dec5dvds  17247  karatsuba  17266  sincos4thpi  26847  sincos6thpi  26849  ang180lem2  27143  ang180lem3  27144  asin1  27227  efiatan2  27250  2efiatan  27251  log2cnv  27277  log2ublem2  27280  log2ublem3  27281  log2ub  27282  bclbnd  27612  bposlem8  27623  2lgsoddprmlem3d  27745  ax5seglem7  29518  ipasslem10  31446  siilem1  31458  normlem0  31716  normlem9  31725  bcseqi  31727  polid2i  31764  dfdec100  33467  dpmul100  33509  dpmul1000  33511  dpexpp1  33520  dpmul4  33526  quad3  36521  iexpire  36592  mulassnni  43129  sn-1ticom  43579  sn-0tie0  43608  fourierswlem  47333  fouriersw  47334  cos5t  48018  goldpolyfactor  48020  goldratmolem2  48026  goldratmolem3  48027  41prothprm  48797  tgoldbachlt  49007