Theorem mulassi 10261

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

Syntax hints:   = wceq 1632   ∈ wcel 2139  (class class class)co 6814  ℂcc 10146   · cmul 10153

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

This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1074

This theorem is referenced by:  8th4div3  11464  numma  11769  decbin0  11894  sq4e2t8  13176  3dec  13264  3decOLD  13267  faclbnd4lem1  13294  ef01bndlem  15133  3dvdsdec  15276  3dvdsdecOLD  15277  3dvds2dec  15278  3dvds2decOLD  15279  dec5dvds  15990  karatsuba  16014  karatsubaOLD  16015  sincos4thpi  24485  sincos6thpi  24487  ang180lem2  24760  ang180lem3  24761  asin1  24841  efiatan2  24864  2efiatan  24865  log2cnv  24891  log2ublem2  24894  log2ublem3  24895  log2ub  24896  bclbnd  25225  bposlem8  25236  2lgsoddprmlem3d  25358  ax5seglem7  26035  ipasslem10  28024  siilem1  28036  normlem0  28296  normlem9  28305  bcseqi  28307  polid2i  28344  dfdec100  29906  dpmul100  29935  dpmul1000  29937  dpexpp1  29946  dpmul4  29952  quad3  31892  iexpire  31949  fourierswlem  40968  fouriersw  40969  41prothprm  42064  tgoldbachlt  42232  tgoldbachltOLD  42238