Theorem mul32d 11390

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068   · cmul 11075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-mulcom 11134  ax-mulass 11136

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395

This theorem is referenced by:  conjmul  11905  modmul1  13934  binom3  14234  bernneq  14239  expmulnbnd  14245  discr  14250  bcm1k  14325  bcp1n  14326  reccn2  15607  binomlem  15842  binomfallfaclem2  16053  tanadd  16182  eirrlem  16219  dvds2ln  16306  bezoutlem4  16559  divgcdcoprm0  16682  modprm0  16824  nrginvrcnlem  24731  tcphcphlem2  25278  csbren  25441  radcnvlem1  26453  tanarg  26661  cxpeq  26799  quad2  26881  binom4  26892  dquartlem2  26894  dquart  26895  quart1lem  26897  dvatan  26977  log2cnv  26986  basellem8  27129  bcmono  27318  gausslemma2d  27415  lgsquadlem1  27421  2lgslem3b  27438  2lgslem3c  27439  2lgslem3d  27440  rplogsumlem1  27525  dchrisumlem2  27531  chpdifbndlem1  27594  selberg3lem1  27598  selberg4  27602  selberg3r  27610  pntrlog2bndlem2  27619  pntrlog2bndlem3  27620  pntrlog2bndlem5  27622  pntlemf  27646  pntlemo  27648  ostth2lem1  27659  ostth2lem3  27676  zringfrac  33711  constrrtcc  33993  logdivsqrle  34908  circum  35988  lcmineqlem8  42617  lcmineqlem12  42621  flt4lem5f  43203  jm2.25  43540  jm2.27c  43548  binomcxplemnotnn0  44896  dvasinbx  46458  stirlinglem3  46614  dirkercncflem2  46642  cevathlem1  47405  itschlc0yqe  49346