Theorem mulassd 8069

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167  (class class class)co 5925  ℂcc 7896   · cmul 7903

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 8001

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

This theorem is referenced by:  ltmul1  8638  recexap  8699  mulap0  8700  mulcanapd  8707  receuap  8715  divmulasscomap  8742  divdivdivap  8759  divmuleqap  8763  conjmulap  8775  apmul1  8834  qapne  9732  modqmul1  10488  modqdi  10503  expadd  10692  mulbinom2  10767  binom3  10768  faclbnd  10852  faclbnd6  10855  bcm1k  10871  bcp1nk  10873  bcval5  10874  crre  11041  remullem  11055  resqrexlemcalc1  11198  resqrexlemnm  11202  amgm2  11302  binomlem  11667  geo2sum  11698  mertenslemi1  11719  clim2prod  11723  sinadd  11920  tanaddap  11923  dvdsmulcr  12005  dvdsmulgcd  12219  qredeq  12291  2sqpwodd  12371  pcaddlem  12535  prmpwdvds  12551  dvexp  15055  dvply1  15109  tangtx  15182  cxpmul  15256  binom4  15323  perfectlem1  15343  perfectlem2  15344  perfect  15345  lgsneg  15373  gausslemma2dlem6  15416  lgseisenlem1  15419  lgseisenlem2  15420  lgseisenlem3  15421  lgseisenlem4  15422  lgsquad2lem1  15430  lgsquad3  15433  2lgslem3a  15442  2lgslem3b  15443  2lgslem3c  15444  2lgslem3d  15445  2lgsoddprmlem2  15455  2sqlem3  15466