Theorem mulassd 8138

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

Syntax hints:   → wi 4   = wceq 1375   ∈ wcel 2180  (class class class)co 5974  ℂcc 7965   · cmul 7972

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 8070

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

This theorem is referenced by:  ltmul1  8707  recexap  8768  mulap0  8769  mulcanapd  8776  receuap  8784  divmulasscomap  8811  divdivdivap  8828  divmuleqap  8832  conjmulap  8844  apmul1  8903  qapne  9802  modqmul1  10566  modqdi  10581  expadd  10770  mulbinom2  10845  binom3  10846  faclbnd  10930  faclbnd6  10933  bcm1k  10949  bcp1nk  10951  bcval5  10952  crre  11334  remullem  11348  resqrexlemcalc1  11491  resqrexlemnm  11495  amgm2  11595  binomlem  11960  geo2sum  11991  mertenslemi1  12012  clim2prod  12016  sinadd  12213  tanaddap  12216  dvdsmulcr  12298  dvdsmulgcd  12512  qredeq  12584  2sqpwodd  12664  pcaddlem  12828  prmpwdvds  12844  dvexp  15350  dvply1  15404  tangtx  15477  cxpmul  15551  binom4  15618  perfectlem1  15638  perfectlem2  15639  perfect  15640  lgsneg  15668  gausslemma2dlem6  15711  lgseisenlem1  15714  lgseisenlem2  15715  lgseisenlem3  15716  lgseisenlem4  15717  lgsquad2lem1  15725  lgsquad3  15728  2lgslem3a  15737  2lgslem3b  15738  2lgslem3c  15739  2lgslem3d  15740  2lgsoddprmlem2  15750  2sqlem3  15761