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 1374	1 ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7358  ℂcc 11025   · cmul 11032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-mulcom 11091  ax-mulass 11093

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6446  df-fv 6498  df-ov 7361

This theorem is referenced by:  conjmul  11859  modmul1  13848  binom3  14148  bernneq  14153  expmulnbnd  14159  discr  14164  bcm1k  14239  bcp1n  14240  reccn2  15521  binomlem  15753  binomfallfaclem2  15964  tanadd  16093  eirrlem  16130  dvds2ln  16217  bezoutlem4  16470  divgcdcoprm0  16593  modprm0  16734  nrginvrcnlem  24634  tcphcphlem2  25181  csbren  25344  radcnvlem1  26362  tanarg  26568  cxpeq  26707  quad2  26789  binom4  26800  dquartlem2  26802  dquart  26803  quart1lem  26805  dvatan  26885  log2cnv  26894  basellem8  27038  bcmono  27228  gausslemma2d  27325  lgsquadlem1  27331  2lgslem3b  27348  2lgslem3c  27349  2lgslem3d  27350  rplogsumlem1  27435  dchrisumlem2  27441  chpdifbndlem1  27504  selberg3lem1  27508  selberg4  27512  selberg3r  27520  pntrlog2bndlem2  27529  pntrlog2bndlem3  27530  pntrlog2bndlem5  27532  pntlemf  27556  pntlemo  27558  ostth2lem1  27569  ostth2lem3  27586  zringfrac  33619  constrrtcc  33885  logdivsqrle  34800  circum  35862  lcmineqlem8  42467  lcmineqlem12  42471  flt4lem5f  43089  jm2.25  43430  jm2.27c  43438  binomcxplemnotnn0  44786  dvasinbx  46352  stirlinglem3  46508  dirkercncflem2  46536  cevathlem1  47299  itschlc0yqe  49194