Theorem mulassi 11221

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

Syntax hints:   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099   · cmul 11106

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105

This theorem is referenced by:  8th4div3  12465  numma  12761  decbin0  12859  sq4e2t8  14237  3dec  14304  faclbnd4lem1  14331  ef01bndlem  16241  3dvdsdec  16391  3dvds2dec  16392  dec5dvds  17125  karatsuba  17144  sincos4thpi  26656  sincos6thpi  26659  ang180lem2  26953  ang180lem3  26954  asin1  27037  efiatan2  27060  2efiatan  27061  log2cnv  27087  log2ublem2  27090  log2ublem3  27091  log2ub  27092  bclbnd  27422  bposlem8  27433  2lgsoddprmlem3d  27555  ax5seglem7  29263  ipasslem10  31169  siilem1  31181  normlem0  31439  normlem9  31448  bcseqi  31450  polid2i  31487  dfdec100  33152  dpmul100  33194  dpmul1000  33196  dpexpp1  33205  dpmul4  33211  quad3  36140  iexpire  36205  mulassnni  42731  sn-1ticom  43174  sn-0tie0  43203  fourierswlem  46924  fouriersw  46925  cos5t  47593  goldratmolem2  47600  41prothprm  48348  tgoldbachlt  48558