Theorem mulassd 8186

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6010  ℂcc 8013   · cmul 8020

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 8118

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

This theorem is referenced by:  ltmul1  8755  recexap  8816  mulap0  8817  mulcanapd  8824  receuap  8832  divmulasscomap  8859  divdivdivap  8876  divmuleqap  8880  conjmulap  8892  apmul1  8951  qapne  9851  modqmul1  10616  modqdi  10631  expadd  10820  mulbinom2  10895  binom3  10896  faclbnd  10980  faclbnd6  10983  bcm1k  10999  bcp1nk  11001  bcval5  11002  crre  11389  remullem  11403  resqrexlemcalc1  11546  resqrexlemnm  11550  amgm2  11650  binomlem  12015  geo2sum  12046  mertenslemi1  12067  clim2prod  12071  sinadd  12268  tanaddap  12271  dvdsmulcr  12353  dvdsmulgcd  12567  qredeq  12639  2sqpwodd  12719  pcaddlem  12883  prmpwdvds  12899  dvexp  15406  dvply1  15460  tangtx  15533  cxpmul  15607  binom4  15674  perfectlem1  15694  perfectlem2  15695  perfect  15696  lgsneg  15724  gausslemma2dlem6  15767  lgseisenlem1  15770  lgseisenlem2  15771  lgseisenlem3  15772  lgseisenlem4  15773  lgsquad2lem1  15781  lgsquad3  15784  2lgslem3a  15793  2lgslem3b  15794  2lgslem3c  15795  2lgslem3d  15796  2lgsoddprmlem2  15806  2sqlem3  15817