Theorem mulassd 8293

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2203  (class class class)co 6049  ℂcc 8121   · cmul 8128

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 8226

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

This theorem is referenced by:  ltmul1  8862  recexap  8923  mulap0  8924  mulcanapd  8931  receuap  8939  divmulasscomap  8966  divdivdivap  8983  divmuleqap  8987  conjmulap  8999  apmul1  9058  qapne  9967  modqmul1  10735  modqdi  10750  expadd  10939  mulbinom2  11014  binom3  11015  faclbnd  11099  faclbnd6  11102  bcm1k  11118  bcp1nk  11120  bcval5  11121  crre  11535  remullem  11549  resqrexlemcalc1  11692  resqrexlemnm  11696  amgm2  11796  binomlem  12162  geo2sum  12193  mertenslemi1  12214  clim2prod  12218  sinadd  12415  tanaddap  12418  dvdsmulcr  12500  dvdsmulgcd  12714  qredeq  12786  2sqpwodd  12866  pcaddlem  13030  prmpwdvds  13046  dvexp  15563  dvply1  15617  tangtx  15690  cxpmul  15764  binom4  15831  perfectlem1  15854  perfectlem2  15855  perfect  15856  lgsneg  15884  gausslemma2dlem6  15927  lgseisenlem1  15930  lgseisenlem2  15931  lgseisenlem3  15932  lgseisenlem4  15933  lgsquad2lem1  15941  lgsquad3  15944  2lgslem3a  15953  2lgslem3b  15954  2lgslem3c  15955  2lgslem3d  15956  2lgsoddprmlem2  15966  2sqlem3  15977