Theorem mul32d 11343

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   · cmul 11031

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 2708  ax-mulcom 11090  ax-mulass 11092

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361

This theorem is referenced by:  conjmul  11858  modmul1  13847  binom3  14147  bernneq  14152  expmulnbnd  14158  discr  14163  bcm1k  14238  bcp1n  14239  reccn2  15520  binomlem  15752  binomfallfaclem2  15963  tanadd  16092  eirrlem  16129  dvds2ln  16216  bezoutlem4  16469  divgcdcoprm0  16592  modprm0  16733  nrginvrcnlem  24635  tcphcphlem2  25192  csbren  25355  radcnvlem1  26378  tanarg  26584  cxpeq  26723  quad2  26805  binom4  26816  dquartlem2  26818  dquart  26819  quart1lem  26821  dvatan  26901  log2cnv  26910  basellem8  27054  bcmono  27244  gausslemma2d  27341  lgsquadlem1  27347  2lgslem3b  27364  2lgslem3c  27365  2lgslem3d  27366  rplogsumlem1  27451  dchrisumlem2  27457  chpdifbndlem1  27520  selberg3lem1  27524  selberg4  27528  selberg3r  27536  pntrlog2bndlem2  27545  pntrlog2bndlem3  27546  pntrlog2bndlem5  27548  pntlemf  27572  pntlemo  27574  ostth2lem1  27585  ostth2lem3  27602  zringfrac  33635  constrrtcc  33892  logdivsqrle  34807  circum  35868  lcmineqlem8  42286  lcmineqlem12  42290  flt4lem5f  42896  jm2.25  43237  jm2.27c  43245  binomcxplemnotnn0  44593  dvasinbx  46160  stirlinglem3  46316  dirkercncflem2  46344  cevathlem1  47107  itschlc0yqe  49002