Theorem mul32d 11438

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116   · cmul 11123

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-mulcom 11182  ax-mulass 11184

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426

This theorem is used by:  conjmul  11950  modmul1  13980  binom3  14280  bernneq  14285  expmulnbnd  14291  discr  14296  bcm1k  14371  bcp1n  14372  reccn2  15674  binomlem  15909  binomfallfaclem2  16119  tanadd  16248  eirrlem  16285  dvds2ln  16372  bezoutlem4  16625  divgcdcoprm0  16748  modprm0  16890  nrginvrcnlem  24885  tcphcphlem2  25432  csbren  25595  radcnvlem1  26613  tanarg  26821  cxpeq  26959  quad2  27041  binom4  27052  dquartlem2  27054  dquart  27055  quart1lem  27057  dvatan  27137  log2cnv  27146  basellem8  27289  bcmono  27478  gausslemma2d  27575  lgsquadlem1  27581  2lgslem3b  27598  2lgslem3c  27599  2lgslem3d  27600  rplogsumlem1  27685  dchrisumlem2  27691  chpdifbndlem1  27754  selberg3lem1  27758  selberg4  27762  selberg3r  27770  pntrlog2bndlem2  27779  pntrlog2bndlem3  27780  pntrlog2bndlem5  27782  pntlemf  27806  pntlemo  27808  ostth2lem1  27819  ostth2lem3  27836  zringfrac  33875  constrrtcc  34156  logdivsqrle  35069  circum  36187  lcmineqlem8  42844  lcmineqlem12  42848  flt4lem5f  43430  jm2.25  43767  jm2.27c  43775  binomcxplemnotnn0  45107  dvasinbx  46675  stirlinglem3  46831  dirkercncflem2  46859  cevathlem1  47622  itschlc0yqe  49581