Theorem mulassd 8203

Description: Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
addassd.3	⊢ (𝜑 → 𝐶 ∈ ℂ)

Assertion

Ref	Expression
mulassd	⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Proof of Theorem mulassd

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addassd.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		mulass 8163	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1273	1 ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202  (class class class)co 6018  ℂcc 8030   · cmul 8037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-mulass 8135

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  ltmul1  8772  recexap  8833  mulap0  8834  mulcanapd  8841  receuap  8849  divmulasscomap  8876  divdivdivap  8893  divmuleqap  8897  conjmulap  8909  apmul1  8968  qapne  9873  modqmul1  10640  modqdi  10655  expadd  10844  mulbinom2  10919  binom3  10920  faclbnd  11004  faclbnd6  11007  bcm1k  11023  bcp1nk  11025  bcval5  11026  crre  11419  remullem  11433  resqrexlemcalc1  11576  resqrexlemnm  11580  amgm2  11680  binomlem  12046  geo2sum  12077  mertenslemi1  12098  clim2prod  12102  sinadd  12299  tanaddap  12302  dvdsmulcr  12384  dvdsmulgcd  12598  qredeq  12670  2sqpwodd  12750  pcaddlem  12914  prmpwdvds  12930  dvexp  15438  dvply1  15492  tangtx  15565  cxpmul  15639  binom4  15706  perfectlem1  15726  perfectlem2  15727  perfect  15728  lgsneg  15756  gausslemma2dlem6  15799  lgseisenlem1  15802  lgseisenlem2  15803  lgseisenlem3  15804  lgseisenlem4  15805  lgsquad2lem1  15813  lgsquad3  15816  2lgslem3a  15825  2lgslem3b  15826  2lgslem3c  15827  2lgslem3d  15828  2lgsoddprmlem2  15838  2sqlem3  15849