Theorem mulassi 11185

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

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

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

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

This theorem is referenced by:  8th4div3  12402  numma  12693  decbin0  12789  sq4e2t8  14164  3dec  14231  faclbnd4lem1  14258  ef01bndlem  16152  3dvdsdec  16302  3dvds2dec  16303  dec5dvds  17035  karatsuba  17054  sincos4thpi  26422  sincos6thpi  26425  ang180lem2  26720  ang180lem3  26721  asin1  26804  efiatan2  26827  2efiatan  26828  log2cnv  26854  log2ublem2  26857  log2ublem3  26858  log2ub  26859  bclbnd  27191  bposlem8  27202  2lgsoddprmlem3d  27324  ax5seglem7  28862  ipasslem10  30768  siilem1  30780  normlem0  31038  normlem9  31047  bcseqi  31049  polid2i  31086  dfdec100  32755  dpmul100  32817  dpmul1000  32819  dpexpp1  32828  dpmul4  32834  quad3  35657  iexpire  35722  mulassnni  41974  sn-1ticom  42423  sn-0tie0  42439  fourierswlem  46228  fouriersw  46229  41prothprm  47620  tgoldbachlt  47817