Theorem mul32d 11115

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800   · cmul 10807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-mulcom 10866  ax-mulass 10868

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  conjmul  11622  modmul1  13572  binom3  13867  bernneq  13872  expmulnbnd  13878  discr  13883  bcm1k  13957  bcp1n  13958  reccn2  15234  binomlem  15469  binomfallfaclem2  15678  tanadd  15804  eirrlem  15841  dvds2ln  15926  bezoutlem4  16178  divgcdcoprm0  16298  modprm0  16434  nrginvrcnlem  23761  tcphcphlem2  24305  csbren  24468  radcnvlem1  25477  tanarg  25679  cxpeq  25815  quad2  25894  binom4  25905  dquartlem2  25907  dquart  25908  quart1lem  25910  dvatan  25990  log2cnv  25999  basellem8  26142  bcmono  26330  gausslemma2d  26427  lgsquadlem1  26433  2lgslem3b  26450  2lgslem3c  26451  2lgslem3d  26452  rplogsumlem1  26537  dchrisumlem2  26543  chpdifbndlem1  26606  selberg3lem1  26610  selberg4  26614  selberg3r  26622  pntrlog2bndlem2  26631  pntrlog2bndlem3  26632  pntrlog2bndlem5  26634  pntlemf  26658  pntlemo  26660  ostth2lem1  26671  ostth2lem3  26688  logdivsqrle  32530  circum  33532  lcmineqlem8  39972  lcmineqlem12  39976  flt4lem5f  40410  jm2.25  40737  jm2.27c  40745  binomcxplemnotnn0  41863  dvasinbx  43351  stirlinglem3  43507  dirkercncflem2  43535  cevathlem1  44270  itschlc0yqe  45994