Theorem mulassi 11301

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  (class class class)co 7412  ℂcc 11179   · cmul 11186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 11247

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  8th4div3  12547  numma  12844  decbin0  12942  sq4e2t8  14322  3dec  14390  faclbnd4lem1  14417  ef01bndlem  16332  3dvdsdec  16482  3dvds2dec  16483  dec5dvds  17222  karatsuba  17241  sincos4thpi  26824  sincos6thpi  26826  ang180lem2  27120  ang180lem3  27121  asin1  27204  efiatan2  27227  2efiatan  27228  log2cnv  27254  log2ublem2  27257  log2ublem3  27258  log2ub  27259  bclbnd  27589  bposlem8  27600  2lgsoddprmlem3d  27722  ax5seglem7  29495  ipasslem10  31423  siilem1  31435  normlem0  31693  normlem9  31702  bcseqi  31704  polid2i  31741  dfdec100  33403  dpmul100  33445  dpmul1000  33447  dpexpp1  33456  dpmul4  33462  quad3  36404  iexpire  36469  mulassnni  43004  sn-1ticom  43454  sn-0tie0  43483  fourierswlem  47184  fouriersw  47185  cos5t  47869  goldpolyfactor  47871  goldratmolem2  47877  goldratmolem3  47878  41prothprm  48648  tgoldbachlt  48858