Theorem mul32d 11330

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011   · cmul 11018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-mulcom 11077  ax-mulass 11079

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355

This theorem is referenced by:  conjmul  11845  modmul1  13833  binom3  14133  bernneq  14138  expmulnbnd  14144  discr  14149  bcm1k  14224  bcp1n  14225  reccn2  15506  binomlem  15738  binomfallfaclem2  15949  tanadd  16078  eirrlem  16115  dvds2ln  16202  bezoutlem4  16455  divgcdcoprm0  16578  modprm0  16719  nrginvrcnlem  24607  tcphcphlem2  25164  csbren  25327  radcnvlem1  26350  tanarg  26556  cxpeq  26695  quad2  26777  binom4  26788  dquartlem2  26790  dquart  26791  quart1lem  26793  dvatan  26873  log2cnv  26882  basellem8  27026  bcmono  27216  gausslemma2d  27313  lgsquadlem1  27319  2lgslem3b  27336  2lgslem3c  27337  2lgslem3d  27338  rplogsumlem1  27423  dchrisumlem2  27429  chpdifbndlem1  27492  selberg3lem1  27496  selberg4  27500  selberg3r  27508  pntrlog2bndlem2  27517  pntrlog2bndlem3  27518  pntrlog2bndlem5  27520  pntlemf  27544  pntlemo  27546  ostth2lem1  27557  ostth2lem3  27574  zringfrac  33526  constrrtcc  33769  logdivsqrle  34684  circum  35739  lcmineqlem8  42149  lcmineqlem12  42153  flt4lem5f  42775  jm2.25  43116  jm2.27c  43124  binomcxplemnotnn0  44473  dvasinbx  46042  stirlinglem3  46198  dirkercncflem2  46226  cevathlem1  46989  itschlc0yqe  48885