Theorem mulassi 11145

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026   · cmul 11033

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

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

This theorem is referenced by:  8th4div3  12362  numma  12653  decbin0  12749  sq4e2t8  14124  3dec  14191  faclbnd4lem1  14218  ef01bndlem  16111  3dvdsdec  16261  3dvds2dec  16262  dec5dvds  16994  karatsuba  17013  sincos4thpi  26438  sincos6thpi  26441  ang180lem2  26736  ang180lem3  26737  asin1  26820  efiatan2  26843  2efiatan  26844  log2cnv  26870  log2ublem2  26873  log2ublem3  26874  log2ub  26875  bclbnd  27207  bposlem8  27218  2lgsoddprmlem3d  27340  ax5seglem7  28898  ipasslem10  30801  siilem1  30813  normlem0  31071  normlem9  31080  bcseqi  31082  polid2i  31119  dfdec100  32788  dpmul100  32850  dpmul1000  32852  dpexpp1  32861  dpmul4  32867  quad3  35642  iexpire  35707  mulassnni  41959  sn-1ticom  42408  sn-0tie0  42424  fourierswlem  46212  fouriersw  46213  41prothprm  47604  tgoldbachlt  47801