Theorem mulassd 7813

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

Syntax hints:   → wi 4   = wceq 1332   ∈ wcel 1481  (class class class)co 5782  ℂcc 7642   · cmul 7649

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

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  ltmul1  8378  recexap  8438  mulap0  8439  mulcanapd  8446  receuap  8454  divmulasscomap  8480  divdivdivap  8497  divmuleqap  8501  conjmulap  8513  apmul1  8572  qapne  9458  modqmul1  10181  modqdi  10196  expadd  10366  mulbinom2  10439  binom3  10440  faclbnd  10519  faclbnd6  10522  bcm1k  10538  bcp1nk  10540  bcval5  10541  crre  10661  remullem  10675  resqrexlemcalc1  10818  resqrexlemnm  10822  amgm2  10922  binomlem  11284  geo2sum  11315  mertenslemi1  11336  clim2prod  11340  sinadd  11479  tanaddap  11482  dvdsmulcr  11559  dvdsmulgcd  11749  qredeq  11813  2sqpwodd  11890  dvexp  12883  tangtx  12967  cxpmul  13041