Theorem mulassd 7901

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

Syntax hints:   → wi 4   = wceq 1335   ∈ wcel 2128  (class class class)co 5824  ℂcc 7730   · cmul 7737

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 7835

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

This theorem is referenced by:  ltmul1  8467  recexap  8527  mulap0  8528  mulcanapd  8535  receuap  8543  divmulasscomap  8569  divdivdivap  8586  divmuleqap  8590  conjmulap  8602  apmul1  8661  qapne  9548  modqmul1  10276  modqdi  10291  expadd  10461  mulbinom2  10534  binom3  10535  faclbnd  10615  faclbnd6  10618  bcm1k  10634  bcp1nk  10636  bcval5  10637  crre  10757  remullem  10771  resqrexlemcalc1  10914  resqrexlemnm  10918  amgm2  11018  binomlem  11380  geo2sum  11411  mertenslemi1  11432  clim2prod  11436  sinadd  11633  tanaddap  11636  dvdsmulcr  11717  dvdsmulgcd  11909  qredeq  11973  2sqpwodd  12051  dvexp  13086  tangtx  13170  cxpmul  13244  binom4  13307