Theorem mulassd 7574

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

Syntax hints:   → wi 4   = wceq 1290   ∈ wcel 1439  (class class class)co 5668  ℂcc 7411   · cmul 7418

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

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

This theorem is referenced by:  ltmul1  8132  recexap  8185  mulap0  8186  mulcanapd  8193  receuap  8201  divmulasscomap  8226  divdivdivap  8243  divmuleqap  8247  conjmulap  8259  apmul1  8318  qapne  9187  modqmul1  9847  modqdi  9862  expadd  10060  mulbinom2  10133  binom3  10134  faclbnd  10212  faclbnd6  10215  bcm1k  10231  bcp1nk  10233  ibcval5  10234  crre  10354  remullem  10368  resqrexlemcalc1  10510  resqrexlemnm  10514  amgm2  10614  binomlem  10940  geo2sum  10971  mertenslemi1  10992  sinadd  11090  tanaddap  11093  dvdsmulcr  11167  dvdsmulgcd  11355  qredeq  11419  2sqpwodd  11495