Theorem mulassd 8350

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 8311	. 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 6085  ℂcc 8178   · cmul 8185

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 8283

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

This theorem is used by:  ltmul1  8923  recexap  8984  mulap0  8985  mulcanapd  8992  receuap  9002  divmulasscomap  9029  divdivdivap  9046  divmuleqap  9050  conjmulap  9062  apmul1  9121  qapne  10049  modqmul1  10829  modqdi  10844  expadd  11033  mulbinom2  11108  binom3  11109  faclbnd  11195  faclbnd6  11198  bcm1k  11214  bcp1nk  11216  bcval5  11217  crre  11638  remullem  11652  sq01  11676  resqrexlemcalc1  11796  resqrexlemnm  11800  amgm2  11901  binomlem  12269  geo2sum  12300  mertenslemi1  12321  clim2prod  12325  sinadd  12522  tanaddap  12525  dvdsmulcr  12607  dvdsmulgcd  12821  qredeq  12893  2sqpwodd  12975  pcaddlem  13141  prmpwdvds  13157  dvexp  15903  dvply1  15957  tangtx  16031  logfac  16092  cxpmul  16111  binom4  16185  log2tlbndlog2  16186  chtqub  16262  perfectlem1  16265  perfectlem2  16266  perfect  16267  bcmono  16270  bclbnd  16273  bposlem9  16285  lgsneg  16314  gausslemma2dlem6  16357  lgseisenlem1  16360  lgseisenlem2  16361  lgseisenlem3  16362  lgseisenlem4  16363  lgsquad2lem1  16371  lgsquad3  16374  2lgslem3a  16383  2lgslem3b  16384  2lgslem3c  16385  2lgslem3d  16386  2lgsoddprmlem2  16396  2sqlem3  16407