Theorem mulassd 8208

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

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2201  (class class class)co 6023  ℂcc 8035   · cmul 8042

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 8140

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

This theorem is referenced by:  ltmul1  8777  recexap  8838  mulap0  8839  mulcanapd  8846  receuap  8854  divmulasscomap  8881  divdivdivap  8898  divmuleqap  8902  conjmulap  8914  apmul1  8973  qapne  9878  modqmul1  10645  modqdi  10660  expadd  10849  mulbinom2  10924  binom3  10925  faclbnd  11009  faclbnd6  11012  bcm1k  11028  bcp1nk  11030  bcval5  11031  crre  11440  remullem  11454  resqrexlemcalc1  11597  resqrexlemnm  11601  amgm2  11701  binomlem  12067  geo2sum  12098  mertenslemi1  12119  clim2prod  12123  sinadd  12320  tanaddap  12323  dvdsmulcr  12405  dvdsmulgcd  12619  qredeq  12691  2sqpwodd  12771  pcaddlem  12935  prmpwdvds  12951  dvexp  15464  dvply1  15518  tangtx  15591  cxpmul  15665  binom4  15732  perfectlem1  15752  perfectlem2  15753  perfect  15754  lgsneg  15782  gausslemma2dlem6  15825  lgseisenlem1  15828  lgseisenlem2  15829  lgseisenlem3  15830  lgseisenlem4  15831  lgsquad2lem1  15839  lgsquad3  15842  2lgslem3a  15851  2lgslem3b  15852  2lgslem3c  15853  2lgslem3d  15854  2lgsoddprmlem2  15864  2sqlem3  15875