Theorem mulassi 11155

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   · cmul 11043

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

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

This theorem is referenced by:  8th4div3  12373  numma  12663  decbin0  12759  sq4e2t8  14134  3dec  14201  faclbnd4lem1  14228  ef01bndlem  16121  3dvdsdec  16271  3dvds2dec  16272  dec5dvds  17004  karatsuba  17023  sincos4thpi  26490  sincos6thpi  26493  ang180lem2  26788  ang180lem3  26789  asin1  26872  efiatan2  26895  2efiatan  26896  log2cnv  26922  log2ublem2  26925  log2ublem3  26926  log2ub  26927  bclbnd  27259  bposlem8  27270  2lgsoddprmlem3d  27392  ax5seglem7  29020  ipasslem10  30926  siilem1  30938  normlem0  31196  normlem9  31205  bcseqi  31207  polid2i  31244  dfdec100  32921  dpmul100  32988  dpmul1000  32990  dpexpp1  32999  dpmul4  33005  quad3  35883  iexpire  35948  mulassnni  42350  sn-1ticom  42799  sn-0tie0  42815  fourierswlem  46582  fouriersw  46583  41prothprm  47973  tgoldbachlt  48170