Theorem mulassi 11143

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   · cmul 11031

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

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

This theorem is referenced by:  8th4div3  12361  numma  12651  decbin0  12747  sq4e2t8  14122  3dec  14189  faclbnd4lem1  14216  ef01bndlem  16109  3dvdsdec  16259  3dvds2dec  16260  dec5dvds  16992  karatsuba  17011  sincos4thpi  26478  sincos6thpi  26481  ang180lem2  26776  ang180lem3  26777  asin1  26860  efiatan2  26883  2efiatan  26884  log2cnv  26910  log2ublem2  26913  log2ublem3  26914  log2ub  26915  bclbnd  27247  bposlem8  27258  2lgsoddprmlem3d  27380  ax5seglem7  29008  ipasslem10  30914  siilem1  30926  normlem0  31184  normlem9  31193  bcseqi  31195  polid2i  31232  dfdec100  32911  dpmul100  32978  dpmul1000  32980  dpexpp1  32989  dpmul4  32995  quad3  35864  iexpire  35929  mulassnni  42236  sn-1ticom  42686  sn-0tie0  42702  fourierswlem  46470  fouriersw  46471  41prothprm  47861  tgoldbachlt  48058