Theorem mul32d 11320

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  (class class class)co 7346  ℂcc 11001   · cmul 11008

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 2113  ax-9 2121  ax-ext 2703  ax-mulcom 11067  ax-mulass 11069

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  conjmul  11835  modmul1  13828  binom3  14128  bernneq  14133  expmulnbnd  14139  discr  14144  bcm1k  14219  bcp1n  14220  reccn2  15501  binomlem  15733  binomfallfaclem2  15944  tanadd  16073  eirrlem  16110  dvds2ln  16197  bezoutlem4  16450  divgcdcoprm0  16573  modprm0  16714  nrginvrcnlem  24604  tcphcphlem2  25161  csbren  25324  radcnvlem1  26347  tanarg  26553  cxpeq  26692  quad2  26774  binom4  26785  dquartlem2  26787  dquart  26788  quart1lem  26790  dvatan  26870  log2cnv  26879  basellem8  27023  bcmono  27213  gausslemma2d  27310  lgsquadlem1  27316  2lgslem3b  27333  2lgslem3c  27334  2lgslem3d  27335  rplogsumlem1  27420  dchrisumlem2  27426  chpdifbndlem1  27489  selberg3lem1  27493  selberg4  27497  selberg3r  27505  pntrlog2bndlem2  27514  pntrlog2bndlem3  27515  pntrlog2bndlem5  27517  pntlemf  27541  pntlemo  27543  ostth2lem1  27554  ostth2lem3  27571  zringfrac  33514  constrrtcc  33743  logdivsqrle  34658  circum  35706  lcmineqlem8  42068  lcmineqlem12  42072  flt4lem5f  42689  jm2.25  43031  jm2.27c  43039  binomcxplemnotnn0  44388  dvasinbx  45957  stirlinglem3  46113  dirkercncflem2  46141  cevathlem1  46904  itschlc0yqe  48791