Theorem mulassi 11192

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073   · cmul 11080

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

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

This theorem is referenced by:  8th4div3  12409  numma  12700  decbin0  12796  sq4e2t8  14171  3dec  14238  faclbnd4lem1  14265  ef01bndlem  16159  3dvdsdec  16309  3dvds2dec  16310  dec5dvds  17042  karatsuba  17061  sincos4thpi  26429  sincos6thpi  26432  ang180lem2  26727  ang180lem3  26728  asin1  26811  efiatan2  26834  2efiatan  26835  log2cnv  26861  log2ublem2  26864  log2ublem3  26865  log2ub  26866  bclbnd  27198  bposlem8  27209  2lgsoddprmlem3d  27331  ax5seglem7  28869  ipasslem10  30775  siilem1  30787  normlem0  31045  normlem9  31054  bcseqi  31056  polid2i  31093  dfdec100  32762  dpmul100  32824  dpmul1000  32826  dpexpp1  32835  dpmul4  32841  quad3  35664  iexpire  35729  mulassnni  41981  sn-1ticom  42430  sn-0tie0  42446  fourierswlem  46235  fouriersw  46236  41prothprm  47624  tgoldbachlt  47821