Theorem mul32d 11501

Description: Commutative/associative law that swaps the last two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
muld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcomd.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
addcand.3	⊢ (𝜑 → 𝐶 ∈ ℂ)

Assertion

Ref	Expression
mul32d	⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵))

Proof of Theorem mul32d

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcomd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addcand.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		mul32 11457	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵))
5	1, 2, 3, 4	syl3anc 1398	1 ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7412  ℂcc 11179   · cmul 11186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-mulcom 11245  ax-mulass 11247

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415

This theorem is used by:  conjmul  12015  modmul1  14047  binom3  14348  bernneq  14353  expmulnbnd  14359  discr  14364  bcm1k  14439  bcp1n  14440  reccn2  15744  binomlem  15978  binomfallfaclem2  16186  tanadd  16315  eirrlem  16352  dvds2ln  16439  bezoutlem4  16695  divgcdcoprm0  16820  modprm0  16963  nrginvrcnlem  24990  tcphcphlem2  25537  csbren  25700  radcnvlem1  26722  tanarg  26929  cxpeq  27067  quad2  27149  binom4  27160  dquartlem2  27162  dquart  27163  quart1lem  27165  dvatan  27245  log2cnv  27254  basellem8  27397  bcmono  27586  gausslemma2d  27683  lgsquadlem1  27689  2lgslem3b  27706  2lgslem3c  27707  2lgslem3d  27708  rplogsumlem1  27793  dchrisumlem2  27799  chpdifbndlem1  27862  selberg3lem1  27866  selberg4  27870  selberg3r  27878  pntrlog2bndlem2  27887  pntrlog2bndlem3  27888  pntrlog2bndlem5  27890  pntlemf  27914  pntlemo  27916  ostth2lem1  27927  ostth2lem3  27944  flt4lem5f  27969  zringfrac  34068  constrrtcc  34349  logdivsqrle  35262  circum  36408  lcmineqlem8  43054  lcmineqlem12  43058  jm2.25  43959  jm2.27c  43967  binomcxplemnotnn0  45299  dvasinbx  46874  stirlinglem3  47030  dirkercncflem2  47058  cevathlem1  47821  itschlc0yqe  49816