Theorem mulassi 10995

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

Syntax hints:   = wceq 1539   ∈ wcel 2107  (class class class)co 7284  ℂcc 10878   · cmul 10885

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088

This theorem is referenced by:  8th4div3  12202  numma  12490  decbin0  12586  sq4e2t8  13925  3dec  13989  faclbnd4lem1  14016  ef01bndlem  15902  3dvdsdec  16050  3dvds2dec  16051  dec5dvds  16774  karatsuba  16794  sincos4thpi  25679  sincos6thpi  25681  ang180lem2  25969  ang180lem3  25970  asin1  26053  efiatan2  26076  2efiatan  26077  log2cnv  26103  log2ublem2  26106  log2ublem3  26107  log2ub  26108  bclbnd  26437  bposlem8  26448  2lgsoddprmlem3d  26570  ax5seglem7  27312  ipasslem10  29210  siilem1  29222  normlem0  29480  normlem9  29489  bcseqi  29491  polid2i  29528  dfdec100  31153  dpmul100  31180  dpmul1000  31182  dpexpp1  31191  dpmul4  31197  quad3  33637  iexpire  33710  mulassnni  40002  sn-1ticom  40423  sn-0tie0  40428  sn-inelr  40442  fourierswlem  43778  fouriersw  43779  41prothprm  45082  tgoldbachlt  45279