Theorem mulassi 11208

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

Syntax hints:   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086   · cmul 11093

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103

This theorem is referenced by:  8th4div3  12452  numma  12748  decbin0  12846  sq4e2t8  14223  3dec  14290  faclbnd4lem1  14317  ef01bndlem  16228  3dvdsdec  16378  3dvds2dec  16379  dec5dvds  17112  karatsuba  17131  sincos4thpi  26632  sincos6thpi  26635  ang180lem2  26929  ang180lem3  26930  asin1  27013  efiatan2  27036  2efiatan  27037  log2cnv  27063  log2ublem2  27066  log2ublem3  27067  log2ub  27068  bclbnd  27398  bposlem8  27409  2lgsoddprmlem3d  27531  ax5seglem7  29190  ipasslem10  31096  siilem1  31108  normlem0  31366  normlem9  31375  bcseqi  31377  polid2i  31414  dfdec100  33082  dpmul100  33124  dpmul1000  33126  dpexpp1  33135  dpmul4  33141  quad3  36028  iexpire  36093  mulassnni  42610  sn-1ticom  43051  sn-0tie0  43080  fourierswlem  46803  fouriersw  46804  cos5t  47472  goldratmolem2  47479  41prothprm  48227  tgoldbachlt  48437