Theorem mulassi 11156

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 7367  ℂ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  12397  numma  12688  decbin0  12784  sq4e2t8  14161  3dec  14228  faclbnd4lem1  14255  ef01bndlem  16151  3dvdsdec  16301  3dvds2dec  16302  dec5dvds  17035  karatsuba  17054  sincos4thpi  26477  sincos6thpi  26480  ang180lem2  26774  ang180lem3  26775  asin1  26858  efiatan2  26881  2efiatan  26882  log2cnv  26908  log2ublem2  26911  log2ublem3  26912  log2ub  26913  bclbnd  27243  bposlem8  27254  2lgsoddprmlem3d  27376  ax5seglem7  29004  ipasslem10  30910  siilem1  30922  normlem0  31180  normlem9  31189  bcseqi  31191  polid2i  31228  dfdec100  32903  dpmul100  32956  dpmul1000  32958  dpexpp1  32967  dpmul4  32973  quad3  35852  iexpire  35917  mulassnni  42425  sn-1ticom  42867  sn-0tie0  42896  fourierswlem  46658  fouriersw  46659  cos5t  47327  goldratmolem2  47334  41prothprm  48082  tgoldbachlt  48292