Theorem mulassd 8178

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6007  ℂcc 8005   · cmul 8012

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 8110

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

This theorem is referenced by:  ltmul1  8747  recexap  8808  mulap0  8809  mulcanapd  8816  receuap  8824  divmulasscomap  8851  divdivdivap  8868  divmuleqap  8872  conjmulap  8884  apmul1  8943  qapne  9842  modqmul1  10607  modqdi  10622  expadd  10811  mulbinom2  10886  binom3  10887  faclbnd  10971  faclbnd6  10974  bcm1k  10990  bcp1nk  10992  bcval5  10993  crre  11376  remullem  11390  resqrexlemcalc1  11533  resqrexlemnm  11537  amgm2  11637  binomlem  12002  geo2sum  12033  mertenslemi1  12054  clim2prod  12058  sinadd  12255  tanaddap  12258  dvdsmulcr  12340  dvdsmulgcd  12554  qredeq  12626  2sqpwodd  12706  pcaddlem  12870  prmpwdvds  12886  dvexp  15393  dvply1  15447  tangtx  15520  cxpmul  15594  binom4  15661  perfectlem1  15681  perfectlem2  15682  perfect  15683  lgsneg  15711  gausslemma2dlem6  15754  lgseisenlem1  15757  lgseisenlem2  15758  lgseisenlem3  15759  lgseisenlem4  15760  lgsquad2lem1  15768  lgsquad3  15771  2lgslem3a  15780  2lgslem3b  15781  2lgslem3c  15782  2lgslem3d  15783  2lgsoddprmlem2  15793  2sqlem3  15804