Theorem mulassd 8196

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6013  ℂcc 8023   · cmul 8030

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 8128

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

This theorem is referenced by:  ltmul1  8765  recexap  8826  mulap0  8827  mulcanapd  8834  receuap  8842  divmulasscomap  8869  divdivdivap  8886  divmuleqap  8890  conjmulap  8902  apmul1  8961  qapne  9866  modqmul1  10632  modqdi  10647  expadd  10836  mulbinom2  10911  binom3  10912  faclbnd  10996  faclbnd6  10999  bcm1k  11015  bcp1nk  11017  bcval5  11018  crre  11411  remullem  11425  resqrexlemcalc1  11568  resqrexlemnm  11572  amgm2  11672  binomlem  12037  geo2sum  12068  mertenslemi1  12089  clim2prod  12093  sinadd  12290  tanaddap  12293  dvdsmulcr  12375  dvdsmulgcd  12589  qredeq  12661  2sqpwodd  12741  pcaddlem  12905  prmpwdvds  12921  dvexp  15428  dvply1  15482  tangtx  15555  cxpmul  15629  binom4  15696  perfectlem1  15716  perfectlem2  15717  perfect  15718  lgsneg  15746  gausslemma2dlem6  15789  lgseisenlem1  15792  lgseisenlem2  15793  lgseisenlem3  15794  lgseisenlem4  15795  lgsquad2lem1  15803  lgsquad3  15806  2lgslem3a  15815  2lgslem3b  15816  2lgslem3c  15817  2lgslem3d  15818  2lgsoddprmlem2  15828  2sqlem3  15839