Theorem mulassd 8349

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 8310	. 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 8177   · cmul 8184

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 8282

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

This theorem is used by:  ltmul1  8922  recexap  8983  mulap0  8984  mulcanapd  8991  receuap  9001  divmulasscomap  9028  divdivdivap  9045  divmuleqap  9049  conjmulap  9061  apmul1  9120  qapne  10048  modqmul1  10827  modqdi  10842  expadd  11031  mulbinom2  11106  binom3  11107  faclbnd  11193  faclbnd6  11196  bcm1k  11212  bcp1nk  11214  bcval5  11215  crre  11636  remullem  11650  sq01  11674  resqrexlemcalc1  11794  resqrexlemnm  11798  amgm2  11899  binomlem  12266  geo2sum  12297  mertenslemi1  12318  clim2prod  12322  sinadd  12519  tanaddap  12522  dvdsmulcr  12604  dvdsmulgcd  12818  qredeq  12890  2sqpwodd  12972  pcaddlem  13138  prmpwdvds  13154  dvexp  15861  dvply1  15915  tangtx  15989  logfac  16048  cxpmul  16067  binom4  16138  log2tlbndlog2  16139  chtqub  16215  perfectlem1  16218  perfectlem2  16219  perfect  16220  bcmono  16223  bclbnd  16226  lgsneg  16262  gausslemma2dlem6  16305  lgseisenlem1  16308  lgseisenlem2  16309  lgseisenlem3  16310  lgseisenlem4  16311  lgsquad2lem1  16319  lgsquad3  16322  2lgslem3a  16331  2lgslem3b  16332  2lgslem3c  16333  2lgslem3d  16334  2lgsoddprmlem2  16344  2sqlem3  16355