Theorem mulassd 8356

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6088  ℂcc 8184   · cmul 8191

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-mulass 8289

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

This theorem is used by:  ltmul1  8929  recexap  8990  mulap0  8991  mulcanapd  8998  receuap  9008  divmulasscomap  9035  divdivdivap  9052  divmuleqap  9056  conjmulap  9068  apmul1  9127  qapne  10056  modqmul1  10836  modqdi  10851  expadd  11040  mulbinom2  11115  binom3  11116  faclbnd  11202  faclbnd6  11205  bcm1k  11221  bcp1nk  11223  bcval5  11224  crre  11645  remullem  11659  sq01  11683  resqrexlemcalc1  11803  resqrexlemnm  11807  amgm2  11908  binomlem  12276  geo2sum  12307  mertenslemi1  12328  clim2prod  12332  sinadd  12529  tanaddap  12532  dvdsmulcr  12614  dvdsmulgcd  12828  qredeq  12900  2sqpwodd  12982  pcaddlem  13148  prmpwdvds  13164  dvexp  15949  dvply1  16003  tangtx  16077  logfac  16138  cxpmul  16157  binom4  16231  log2tlbndlog2  16232  chtqub  16308  perfectlem1  16311  perfectlem2  16312  perfect  16313  bcmono  16316  bclbnd  16319  bposlem9  16331  lgsneg  16360  gausslemma2dlem6  16403  lgseisenlem1  16406  lgseisenlem2  16407  lgseisenlem3  16408  lgseisenlem4  16409  lgsquad2lem1  16417  lgsquad3  16420  2lgslem3a  16429  2lgslem3b  16430  2lgslem3c  16431  2lgslem3d  16432  2lgsoddprmlem2  16442  2sqlem3  16453