Theorem mulassd 8343

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

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6079  ℂcc 8171   · cmul 8178

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 8276

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

This theorem is referenced by:  ltmul1  8914  recexap  8975  mulap0  8976  mulcanapd  8983  receuap  8993  divmulasscomap  9020  divdivdivap  9037  divmuleqap  9041  conjmulap  9053  apmul1  9112  qapne  10022  modqmul1  10797  modqdi  10812  expadd  11001  mulbinom2  11076  binom3  11077  faclbnd  11162  faclbnd6  11165  bcm1k  11181  bcp1nk  11183  bcval5  11184  crre  11605  remullem  11619  sq01  11643  resqrexlemcalc1  11763  resqrexlemnm  11767  amgm2  11867  binomlem  12233  geo2sum  12264  mertenslemi1  12285  clim2prod  12289  sinadd  12486  tanaddap  12489  dvdsmulcr  12571  dvdsmulgcd  12785  qredeq  12857  2sqpwodd  12937  pcaddlem  13101  prmpwdvds  13117  dvexp  15795  dvply1  15849  tangtx  15922  logfac  15978  cxpmul  15997  binom4  16064  log2tlbndlog2  16065  perfectlem1  16096  perfectlem2  16097  perfect  16098  lgsneg  16126  gausslemma2dlem6  16169  lgseisenlem1  16172  lgseisenlem2  16173  lgseisenlem3  16174  lgseisenlem4  16175  lgsquad2lem1  16183  lgsquad3  16186  2lgslem3a  16195  2lgslem3b  16196  2lgslem3c  16197  2lgslem3d  16198  2lgsoddprmlem2  16208  2sqlem3  16219