Theorem mulassd 7980

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  (class class class)co 5874  ℂcc 7808   · cmul 7815

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 7913

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

This theorem is referenced by:  ltmul1  8548  recexap  8609  mulap0  8610  mulcanapd  8617  receuap  8625  divmulasscomap  8652  divdivdivap  8669  divmuleqap  8673  conjmulap  8685  apmul1  8744  qapne  9638  modqmul1  10376  modqdi  10391  expadd  10561  mulbinom2  10636  binom3  10637  faclbnd  10720  faclbnd6  10723  bcm1k  10739  bcp1nk  10741  bcval5  10742  crre  10865  remullem  10879  resqrexlemcalc1  11022  resqrexlemnm  11026  amgm2  11126  binomlem  11490  geo2sum  11521  mertenslemi1  11542  clim2prod  11546  sinadd  11743  tanaddap  11746  dvdsmulcr  11827  dvdsmulgcd  12025  qredeq  12095  2sqpwodd  12175  pcaddlem  12337  prmpwdvds  12352  dvexp  14111  tangtx  14195  cxpmul  14269  binom4  14333  lgsneg  14361  lgseisenlem1  14386  lgseisenlem2  14387  2lgsoddprmlem2  14390  2sqlem3  14400