Theorem mul32d 11450

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7410  ℂcc 11132   · cmul 11139

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 2708  ax-mulcom 11198  ax-mulass 11200

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413

This theorem is referenced by:  conjmul  11963  modmul1  13947  binom3  14247  bernneq  14252  expmulnbnd  14258  discr  14263  bcm1k  14338  bcp1n  14339  reccn2  15618  binomlem  15850  binomfallfaclem2  16061  tanadd  16190  eirrlem  16227  dvds2ln  16313  bezoutlem4  16566  divgcdcoprm0  16689  modprm0  16830  nrginvrcnlem  24635  tcphcphlem2  25193  csbren  25356  radcnvlem1  26379  tanarg  26585  cxpeq  26724  quad2  26806  binom4  26817  dquartlem2  26819  dquart  26820  quart1lem  26822  dvatan  26902  log2cnv  26911  basellem8  27055  bcmono  27245  gausslemma2d  27342  lgsquadlem1  27348  2lgslem3b  27365  2lgslem3c  27366  2lgslem3d  27367  rplogsumlem1  27452  dchrisumlem2  27458  chpdifbndlem1  27521  selberg3lem1  27525  selberg4  27529  selberg3r  27537  pntrlog2bndlem2  27546  pntrlog2bndlem3  27547  pntrlog2bndlem5  27549  pntlemf  27573  pntlemo  27575  ostth2lem1  27586  ostth2lem3  27603  zringfrac  33574  constrrtcc  33774  logdivsqrle  34687  circum  35701  lcmineqlem8  42054  lcmineqlem12  42058  flt4lem5f  42647  jm2.25  42990  jm2.27c  42998  binomcxplemnotnn0  44347  dvasinbx  45916  stirlinglem3  46072  dirkercncflem2  46100  cevathlem1  46863  itschlc0yqe  48707