Theorem mulassd 8313

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141   · cmul 8148

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 8246

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

This theorem is referenced by:  ltmul1  8884  recexap  8945  mulap0  8946  mulcanapd  8953  receuap  8963  divmulasscomap  8990  divdivdivap  9007  divmuleqap  9011  conjmulap  9023  apmul1  9082  qapne  9992  modqmul1  10766  modqdi  10781  expadd  10970  mulbinom2  11045  binom3  11046  faclbnd  11131  faclbnd6  11134  bcm1k  11150  bcp1nk  11152  bcval5  11153  crre  11570  remullem  11584  resqrexlemcalc1  11727  resqrexlemnm  11731  amgm2  11831  binomlem  12197  geo2sum  12228  mertenslemi1  12249  clim2prod  12253  sinadd  12450  tanaddap  12453  dvdsmulcr  12535  dvdsmulgcd  12749  qredeq  12821  2sqpwodd  12901  pcaddlem  13065  prmpwdvds  13081  dvexp  15705  dvply1  15759  tangtx  15832  cxpmul  15906  binom4  15973  perfectlem1  15996  perfectlem2  15997  perfect  15998  lgsneg  16026  gausslemma2dlem6  16069  lgseisenlem1  16072  lgseisenlem2  16073  lgseisenlem3  16074  lgseisenlem4  16075  lgsquad2lem1  16083  lgsquad3  16086  2lgslem3a  16095  2lgslem3b  16096  2lgslem3c  16097  2lgslem3d  16098  2lgsoddprmlem2  16108  2sqlem3  16119