Theorem mulassi 10654

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

Syntax hints:   = wceq 1537   ∈ wcel 2114  (class class class)co 7158  ℂcc 10537   · cmul 10544

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085

This theorem is referenced by:  8th4div3  11860  numma  12145  decbin0  12241  sq4e2t8  13565  3dec  13629  faclbnd4lem1  13656  ef01bndlem  15539  3dvdsdec  15683  3dvds2dec  15684  dec5dvds  16402  karatsuba  16422  sincos4thpi  25101  sincos6thpi  25103  ang180lem2  25390  ang180lem3  25391  asin1  25474  efiatan2  25497  2efiatan  25498  log2cnv  25524  log2ublem2  25527  log2ublem3  25528  log2ub  25529  bclbnd  25858  bposlem8  25869  2lgsoddprmlem3d  25991  ax5seglem7  26723  ipasslem10  28618  siilem1  28630  normlem0  28888  normlem9  28897  bcseqi  28899  polid2i  28936  dfdec100  30548  dpmul100  30575  dpmul1000  30577  dpexpp1  30586  dpmul4  30592  quad3  32915  iexpire  32969  fourierswlem  42522  fouriersw  42523  41prothprm  43791  tgoldbachlt  43988