Theorem mulassi 11190

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

Syntax hints:   = wceq 1559   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068   · cmul 11075

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1099

This theorem is referenced by:  8th4div3  12438  numma  12734  decbin0  12832  sq4e2t8  14209  3dec  14276  faclbnd4lem1  14303  ef01bndlem  16199  3dvdsdec  16349  3dvds2dec  16350  dec5dvds  17083  karatsuba  17102  sincos4thpi  26555  sincos6thpi  26558  ang180lem2  26852  ang180lem3  26853  asin1  26936  efiatan2  26959  2efiatan  26960  log2cnv  26986  log2ublem2  26989  log2ublem3  26990  log2ub  26991  bclbnd  27321  bposlem8  27332  2lgsoddprmlem3d  27454  ax5seglem7  29082  ipasslem10  30988  siilem1  31000  normlem0  31258  normlem9  31267  bcseqi  31269  polid2i  31306  dfdec100  32982  dpmul100  33035  dpmul1000  33037  dpexpp1  33046  dpmul4  33052  quad3  35984  iexpire  36049  mulassnni  42567  sn-1ticom  43008  sn-0tie0  43037  fourierswlem  46768  fouriersw  46769  cos5t  47437  goldratmolem2  47444  41prothprm  48192  tgoldbachlt  48402