Theorem mulassd 8050

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167  (class class class)co 5922  ℂcc 7877   · cmul 7884

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 7982

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

This theorem is referenced by:  ltmul1  8619  recexap  8680  mulap0  8681  mulcanapd  8688  receuap  8696  divmulasscomap  8723  divdivdivap  8740  divmuleqap  8744  conjmulap  8756  apmul1  8815  qapne  9713  modqmul1  10469  modqdi  10484  expadd  10673  mulbinom2  10748  binom3  10749  faclbnd  10833  faclbnd6  10836  bcm1k  10852  bcp1nk  10854  bcval5  10855  crre  11022  remullem  11036  resqrexlemcalc1  11179  resqrexlemnm  11183  amgm2  11283  binomlem  11648  geo2sum  11679  mertenslemi1  11700  clim2prod  11704  sinadd  11901  tanaddap  11904  dvdsmulcr  11986  dvdsmulgcd  12192  qredeq  12264  2sqpwodd  12344  pcaddlem  12508  prmpwdvds  12524  dvexp  14947  dvply1  15001  tangtx  15074  cxpmul  15148  binom4  15215  perfectlem1  15235  perfectlem2  15236  perfect  15237  lgsneg  15265  gausslemma2dlem6  15308  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgseisenlem4  15314  lgsquad2lem1  15322  lgsquad3  15325  2lgslem3a  15334  2lgslem3b  15335  2lgslem3c  15336  2lgslem3d  15337  2lgsoddprmlem2  15347  2sqlem3  15358