Theorem mul32d 11423

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  (class class class)co 7408  ℂcc 11107   · cmul 11114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-mulcom 11173  ax-mulass 11175

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7411

This theorem is referenced by:  conjmul  11930  modmul1  13888  binom3  14186  bernneq  14191  expmulnbnd  14197  discr  14202  bcm1k  14274  bcp1n  14275  reccn2  15540  binomlem  15774  binomfallfaclem2  15983  tanadd  16109  eirrlem  16146  dvds2ln  16231  bezoutlem4  16483  divgcdcoprm0  16601  modprm0  16737  nrginvrcnlem  24207  tcphcphlem2  24752  csbren  24915  radcnvlem1  25924  tanarg  26126  cxpeq  26262  quad2  26341  binom4  26352  dquartlem2  26354  dquart  26355  quart1lem  26357  dvatan  26437  log2cnv  26446  basellem8  26589  bcmono  26777  gausslemma2d  26874  lgsquadlem1  26880  2lgslem3b  26897  2lgslem3c  26898  2lgslem3d  26899  rplogsumlem1  26984  dchrisumlem2  26990  chpdifbndlem1  27053  selberg3lem1  27057  selberg4  27061  selberg3r  27069  pntrlog2bndlem2  27078  pntrlog2bndlem3  27079  pntrlog2bndlem5  27081  pntlemf  27105  pntlemo  27107  ostth2lem1  27118  ostth2lem3  27135  logdivsqrle  33657  circum  34654  lcmineqlem8  40896  lcmineqlem12  40900  flt4lem5f  41400  jm2.25  41728  jm2.27c  41736  binomcxplemnotnn0  43105  dvasinbx  44626  stirlinglem3  44782  dirkercncflem2  44810  cevathlem1  45573  itschlc0yqe  47436