Theorem mul32d 11424

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108   · cmul 11115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-mulcom 11174  ax-mulass 11176

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412

This theorem is referenced by:  conjmul  11931  modmul1  13889  binom3  14187  bernneq  14192  expmulnbnd  14198  discr  14203  bcm1k  14275  bcp1n  14276  reccn2  15541  binomlem  15775  binomfallfaclem2  15984  tanadd  16110  eirrlem  16147  dvds2ln  16232  bezoutlem4  16484  divgcdcoprm0  16602  modprm0  16738  nrginvrcnlem  24208  tcphcphlem2  24753  csbren  24916  radcnvlem1  25925  tanarg  26127  cxpeq  26265  quad2  26344  binom4  26355  dquartlem2  26357  dquart  26358  quart1lem  26360  dvatan  26440  log2cnv  26449  basellem8  26592  bcmono  26780  gausslemma2d  26877  lgsquadlem1  26883  2lgslem3b  26900  2lgslem3c  26901  2lgslem3d  26902  rplogsumlem1  26987  dchrisumlem2  26993  chpdifbndlem1  27056  selberg3lem1  27060  selberg4  27064  selberg3r  27072  pntrlog2bndlem2  27081  pntrlog2bndlem3  27082  pntrlog2bndlem5  27084  pntlemf  27108  pntlemo  27110  ostth2lem1  27121  ostth2lem3  27138  logdivsqrle  33693  circum  34690  lcmineqlem8  40949  lcmineqlem12  40953  flt4lem5f  41447  jm2.25  41786  jm2.27c  41794  binomcxplemnotnn0  43163  dvasinbx  44684  stirlinglem3  44840  dirkercncflem2  44868  cevathlem1  45631  itschlc0yqe  47494