Theorem mulassi 10641

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

Syntax hints:   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524   · cmul 10531

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086

This theorem is referenced by:  8th4div3  11845  numma  12130  decbin0  12226  sq4e2t8  13558  3dec  13622  faclbnd4lem1  13649  ef01bndlem  15529  3dvdsdec  15673  3dvds2dec  15674  dec5dvds  16390  karatsuba  16410  sincos4thpi  25106  sincos6thpi  25108  ang180lem2  25396  ang180lem3  25397  asin1  25480  efiatan2  25503  2efiatan  25504  log2cnv  25530  log2ublem2  25533  log2ublem3  25534  log2ub  25535  bclbnd  25864  bposlem8  25875  2lgsoddprmlem3d  25997  ax5seglem7  26729  ipasslem10  28622  siilem1  28634  normlem0  28892  normlem9  28901  bcseqi  28903  polid2i  28940  dfdec100  30572  dpmul100  30599  dpmul1000  30601  dpexpp1  30610  dpmul4  30616  quad3  33026  iexpire  33080  mulassnni  39274  3lexlogpow5ineq1  39341  sn-1ticom  39571  sn-0tie0  39576  sn-inelr  39590  fourierswlem  42872  fouriersw  42873  41prothprm  44137  tgoldbachlt  44334