Theorem mulassi 11147

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027   · cmul 11034

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

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

This theorem is referenced by:  8th4div3  12388  numma  12679  decbin0  12775  sq4e2t8  14152  3dec  14219  faclbnd4lem1  14246  ef01bndlem  16142  3dvdsdec  16292  3dvds2dec  16293  dec5dvds  17026  karatsuba  17045  sincos4thpi  26490  sincos6thpi  26493  ang180lem2  26787  ang180lem3  26788  asin1  26871  efiatan2  26894  2efiatan  26895  log2cnv  26921  log2ublem2  26924  log2ublem3  26925  log2ub  26926  bclbnd  27257  bposlem8  27268  2lgsoddprmlem3d  27390  ax5seglem7  29018  ipasslem10  30925  siilem1  30937  normlem0  31195  normlem9  31204  bcseqi  31206  polid2i  31243  dfdec100  32918  dpmul100  32971  dpmul1000  32973  dpexpp1  32982  dpmul4  32988  quad3  35868  iexpire  35933  mulassnni  42439  sn-1ticom  42881  sn-0tie0  42910  fourierswlem  46676  fouriersw  46677  41prothprm  48094  tgoldbachlt  48304