Theorem mulassd 8103

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2177  (class class class)co 5951  ℂcc 7930   · cmul 7937

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 8035

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

This theorem is referenced by:  ltmul1  8672  recexap  8733  mulap0  8734  mulcanapd  8741  receuap  8749  divmulasscomap  8776  divdivdivap  8793  divmuleqap  8797  conjmulap  8809  apmul1  8868  qapne  9767  modqmul1  10529  modqdi  10544  expadd  10733  mulbinom2  10808  binom3  10809  faclbnd  10893  faclbnd6  10896  bcm1k  10912  bcp1nk  10914  bcval5  10915  crre  11212  remullem  11226  resqrexlemcalc1  11369  resqrexlemnm  11373  amgm2  11473  binomlem  11838  geo2sum  11869  mertenslemi1  11890  clim2prod  11894  sinadd  12091  tanaddap  12094  dvdsmulcr  12176  dvdsmulgcd  12390  qredeq  12462  2sqpwodd  12542  pcaddlem  12706  prmpwdvds  12722  dvexp  15227  dvply1  15281  tangtx  15354  cxpmul  15428  binom4  15495  perfectlem1  15515  perfectlem2  15516  perfect  15517  lgsneg  15545  gausslemma2dlem6  15588  lgseisenlem1  15591  lgseisenlem2  15592  lgseisenlem3  15593  lgseisenlem4  15594  lgsquad2lem1  15602  lgsquad3  15605  2lgslem3a  15614  2lgslem3b  15615  2lgslem3c  15616  2lgslem3d  15617  2lgsoddprmlem2  15627  2sqlem3  15638