Theorem mul32d 11355

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   · cmul 11043

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 11102  ax-mulass 11104

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371

This theorem is referenced by:  conjmul  11870  modmul1  13859  binom3  14159  bernneq  14164  expmulnbnd  14170  discr  14175  bcm1k  14250  bcp1n  14251  reccn2  15532  binomlem  15764  binomfallfaclem2  15975  tanadd  16104  eirrlem  16141  dvds2ln  16228  bezoutlem4  16481  divgcdcoprm0  16604  modprm0  16745  nrginvrcnlem  24647  tcphcphlem2  25204  csbren  25367  radcnvlem1  26390  tanarg  26596  cxpeq  26735  quad2  26817  binom4  26828  dquartlem2  26830  dquart  26831  quart1lem  26833  dvatan  26913  log2cnv  26922  basellem8  27066  bcmono  27256  gausslemma2d  27353  lgsquadlem1  27359  2lgslem3b  27376  2lgslem3c  27377  2lgslem3d  27378  rplogsumlem1  27463  dchrisumlem2  27469  chpdifbndlem1  27532  selberg3lem1  27536  selberg4  27540  selberg3r  27548  pntrlog2bndlem2  27557  pntrlog2bndlem3  27558  pntrlog2bndlem5  27560  pntlemf  27584  pntlemo  27586  ostth2lem1  27597  ostth2lem3  27614  zringfrac  33646  constrrtcc  33912  logdivsqrle  34827  circum  35887  lcmineqlem8  42400  lcmineqlem12  42404  flt4lem5f  43009  jm2.25  43350  jm2.27c  43358  binomcxplemnotnn0  44706  dvasinbx  46272  stirlinglem3  46428  dirkercncflem2  46456  cevathlem1  47219  itschlc0yqe  49114