Theorem mulassd 7984

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 7945	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1238	1 ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  (class class class)co 5878  ℂcc 7812   · cmul 7819

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 7917

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

This theorem is referenced by:  ltmul1  8552  recexap  8613  mulap0  8614  mulcanapd  8621  receuap  8629  divmulasscomap  8656  divdivdivap  8673  divmuleqap  8677  conjmulap  8689  apmul1  8748  qapne  9642  modqmul1  10380  modqdi  10395  expadd  10565  mulbinom2  10640  binom3  10641  faclbnd  10724  faclbnd6  10727  bcm1k  10743  bcp1nk  10745  bcval5  10746  crre  10869  remullem  10883  resqrexlemcalc1  11026  resqrexlemnm  11030  amgm2  11130  binomlem  11494  geo2sum  11525  mertenslemi1  11546  clim2prod  11550  sinadd  11747  tanaddap  11750  dvdsmulcr  11831  dvdsmulgcd  12029  qredeq  12099  2sqpwodd  12179  pcaddlem  12341  prmpwdvds  12356  dvexp  14315  tangtx  14399  cxpmul  14473  binom4  14537  lgsneg  14565  lgseisenlem1  14590  lgseisenlem2  14591  2lgsoddprmlem2  14594  2sqlem3  14604