Theorem mulassi 11230

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

Syntax hints:   = wceq 1540   ∈ wcel 2105  (class class class)co 7412  ℂcc 11111   · cmul 11118

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

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

This theorem is referenced by:  8th4div3  12437  numma  12726  decbin0  12822  sq4e2t8  14168  3dec  14231  faclbnd4lem1  14258  ef01bndlem  16132  3dvdsdec  16280  3dvds2dec  16281  dec5dvds  17002  karatsuba  17022  sincos4thpi  26260  sincos6thpi  26262  ang180lem2  26552  ang180lem3  26553  asin1  26636  efiatan2  26659  2efiatan  26660  log2cnv  26686  log2ublem2  26689  log2ublem3  26690  log2ub  26691  bclbnd  27020  bposlem8  27031  2lgsoddprmlem3d  27153  ax5seglem7  28461  ipasslem10  30360  siilem1  30372  normlem0  30630  normlem9  30639  bcseqi  30641  polid2i  30678  dfdec100  32304  dpmul100  32331  dpmul1000  32333  dpexpp1  32342  dpmul4  32348  quad3  34954  iexpire  35010  mulassnni  41159  sn-1ticom  41610  sn-0tie0  41615  sn-inelr  41641  fourierswlem  45245  fouriersw  45246  41prothprm  46586  tgoldbachlt  46783