Theorem mul32d 11421

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099   · cmul 11106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-mulcom 11165  ax-mulass 11167

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415

This theorem is referenced by:  conjmul  11933  modmul1  13962  binom3  14262  bernneq  14267  expmulnbnd  14273  discr  14278  bcm1k  14353  bcp1n  14354  reccn2  15650  binomlem  15885  binomfallfaclem2  16095  tanadd  16224  eirrlem  16261  dvds2ln  16348  bezoutlem4  16601  divgcdcoprm0  16724  modprm0  16866  nrginvrcnlem  24829  tcphcphlem2  25376  csbren  25539  radcnvlem1  26554  tanarg  26762  cxpeq  26900  quad2  26982  binom4  26993  dquartlem2  26995  dquart  26996  quart1lem  26998  dvatan  27078  log2cnv  27087  basellem8  27230  bcmono  27419  gausslemma2d  27516  lgsquadlem1  27522  2lgslem3b  27539  2lgslem3c  27540  2lgslem3d  27541  rplogsumlem1  27626  dchrisumlem2  27632  chpdifbndlem1  27695  selberg3lem1  27699  selberg4  27703  selberg3r  27711  pntrlog2bndlem2  27720  pntrlog2bndlem3  27721  pntrlog2bndlem5  27723  pntlemf  27747  pntlemo  27749  ostth2lem1  27760  ostth2lem3  27777  zringfrac  33822  constrrtcc  34103  logdivsqrle  35015  circum  36144  lcmineqlem8  42781  lcmineqlem12  42785  flt4lem5f  43369  jm2.25  43706  jm2.27c  43714  binomcxplemnotnn0  45046  dvasinbx  46614  stirlinglem3  46770  dirkercncflem2  46798  cevathlem1  47561  itschlc0yqe  49517