Theorem mul32d 11469

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106  (class class class)co 7431  ℂcc 11151   · cmul 11158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-mulcom 11217  ax-mulass 11219

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434

This theorem is referenced by:  conjmul  11982  modmul1  13962  binom3  14260  bernneq  14265  expmulnbnd  14271  discr  14276  bcm1k  14351  bcp1n  14352  reccn2  15630  binomlem  15862  binomfallfaclem2  16073  tanadd  16200  eirrlem  16237  dvds2ln  16323  bezoutlem4  16576  divgcdcoprm0  16699  modprm0  16839  nrginvrcnlem  24728  tcphcphlem2  25284  csbren  25447  radcnvlem1  26471  tanarg  26676  cxpeq  26815  quad2  26897  binom4  26908  dquartlem2  26910  dquart  26911  quart1lem  26913  dvatan  26993  log2cnv  27002  basellem8  27146  bcmono  27336  gausslemma2d  27433  lgsquadlem1  27439  2lgslem3b  27456  2lgslem3c  27457  2lgslem3d  27458  rplogsumlem1  27543  dchrisumlem2  27549  chpdifbndlem1  27612  selberg3lem1  27616  selberg4  27620  selberg3r  27628  pntrlog2bndlem2  27637  pntrlog2bndlem3  27638  pntrlog2bndlem5  27640  pntlemf  27664  pntlemo  27666  ostth2lem1  27677  ostth2lem3  27694  zringfrac  33562  constrrtcc  33741  logdivsqrle  34644  circum  35659  lcmineqlem8  42018  lcmineqlem12  42022  flt4lem5f  42644  jm2.25  42988  jm2.27c  42996  binomcxplemnotnn0  44352  dvasinbx  45876  stirlinglem3  46032  dirkercncflem2  46060  cevathlem1  46823  itschlc0yqe  48610