Theorem mulassd 8043

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2164  (class class class)co 5918  ℂcc 7870   · cmul 7877

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 7975

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

This theorem is referenced by:  ltmul1  8611  recexap  8672  mulap0  8673  mulcanapd  8680  receuap  8688  divmulasscomap  8715  divdivdivap  8732  divmuleqap  8736  conjmulap  8748  apmul1  8807  qapne  9704  modqmul1  10448  modqdi  10463  expadd  10652  mulbinom2  10727  binom3  10728  faclbnd  10812  faclbnd6  10815  bcm1k  10831  bcp1nk  10833  bcval5  10834  crre  11001  remullem  11015  resqrexlemcalc1  11158  resqrexlemnm  11162  amgm2  11262  binomlem  11626  geo2sum  11657  mertenslemi1  11678  clim2prod  11682  sinadd  11879  tanaddap  11882  dvdsmulcr  11964  dvdsmulgcd  12162  qredeq  12234  2sqpwodd  12314  pcaddlem  12477  prmpwdvds  12493  dvexp  14860  tangtx  14973  cxpmul  15047  binom4  15111  lgsneg  15140  gausslemma2dlem6  15183  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgseisenlem4  15189  2lgsoddprmlem2  15194  2sqlem3  15204