Theorem mulassd 8067

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167  (class class class)co 5925  ℂcc 7894   · cmul 7901

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 7999

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

This theorem is referenced by:  ltmul1  8636  recexap  8697  mulap0  8698  mulcanapd  8705  receuap  8713  divmulasscomap  8740  divdivdivap  8757  divmuleqap  8761  conjmulap  8773  apmul1  8832  qapne  9730  modqmul1  10486  modqdi  10501  expadd  10690  mulbinom2  10765  binom3  10766  faclbnd  10850  faclbnd6  10853  bcm1k  10869  bcp1nk  10871  bcval5  10872  crre  11039  remullem  11053  resqrexlemcalc1  11196  resqrexlemnm  11200  amgm2  11300  binomlem  11665  geo2sum  11696  mertenslemi1  11717  clim2prod  11721  sinadd  11918  tanaddap  11921  dvdsmulcr  12003  dvdsmulgcd  12217  qredeq  12289  2sqpwodd  12369  pcaddlem  12533  prmpwdvds  12549  dvexp  15031  dvply1  15085  tangtx  15158  cxpmul  15232  binom4  15299  perfectlem1  15319  perfectlem2  15320  perfect  15321  lgsneg  15349  gausslemma2dlem6  15392  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgseisenlem4  15398  lgsquad2lem1  15406  lgsquad3  15409  2lgslem3a  15418  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  2lgsoddprmlem2  15431  2sqlem3  15442