Theorem mul32d 11344

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026   · cmul 11033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-mulcom 11092  ax-mulass 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356

This theorem is referenced by:  conjmul  11859  modmul1  13849  binom3  14149  bernneq  14154  expmulnbnd  14160  discr  14165  bcm1k  14240  bcp1n  14241  reccn2  15522  binomlem  15754  binomfallfaclem2  15965  tanadd  16094  eirrlem  16131  dvds2ln  16218  bezoutlem4  16471  divgcdcoprm0  16594  modprm0  16735  nrginvrcnlem  24595  tcphcphlem2  25152  csbren  25315  radcnvlem1  26338  tanarg  26544  cxpeq  26683  quad2  26765  binom4  26776  dquartlem2  26778  dquart  26779  quart1lem  26781  dvatan  26861  log2cnv  26870  basellem8  27014  bcmono  27204  gausslemma2d  27301  lgsquadlem1  27307  2lgslem3b  27324  2lgslem3c  27325  2lgslem3d  27326  rplogsumlem1  27411  dchrisumlem2  27417  chpdifbndlem1  27480  selberg3lem1  27484  selberg4  27488  selberg3r  27496  pntrlog2bndlem2  27505  pntrlog2bndlem3  27506  pntrlog2bndlem5  27508  pntlemf  27532  pntlemo  27534  ostth2lem1  27545  ostth2lem3  27562  zringfrac  33501  constrrtcc  33701  logdivsqrle  34617  circum  35646  lcmineqlem8  42009  lcmineqlem12  42013  flt4lem5f  42630  jm2.25  42972  jm2.27c  42980  binomcxplemnotnn0  44329  dvasinbx  45902  stirlinglem3  46058  dirkercncflem2  46086  cevathlem1  46849  itschlc0yqe  48746