Theorem mulassd 8302

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205  (class class class)co 6052  ℂcc 8130   · cmul 8137

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 8235

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

This theorem is referenced by:  ltmul1  8871  recexap  8932  mulap0  8933  mulcanapd  8940  receuap  8948  divmulasscomap  8975  divdivdivap  8992  divmuleqap  8996  conjmulap  9008  apmul1  9067  qapne  9977  modqmul1  10746  modqdi  10761  expadd  10950  mulbinom2  11025  binom3  11026  faclbnd  11111  faclbnd6  11114  bcm1k  11130  bcp1nk  11132  bcval5  11133  crre  11550  remullem  11564  resqrexlemcalc1  11707  resqrexlemnm  11711  amgm2  11811  binomlem  12177  geo2sum  12208  mertenslemi1  12229  clim2prod  12233  sinadd  12430  tanaddap  12433  dvdsmulcr  12515  dvdsmulgcd  12729  qredeq  12801  2sqpwodd  12881  pcaddlem  13045  prmpwdvds  13061  dvexp  15625  dvply1  15679  tangtx  15752  cxpmul  15826  binom4  15893  perfectlem1  15916  perfectlem2  15917  perfect  15918  lgsneg  15946  gausslemma2dlem6  15989  lgseisenlem1  15992  lgseisenlem2  15993  lgseisenlem3  15994  lgseisenlem4  15995  lgsquad2lem1  16003  lgsquad3  16006  2lgslem3a  16015  2lgslem3b  16016  2lgslem3c  16017  2lgslem3d  16018  2lgsoddprmlem2  16028  2sqlem3  16039