Theorem mul32d 11408

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086   · cmul 11093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-mulcom 11152  ax-mulass 11154

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403

This theorem is referenced by:  conjmul  11923  modmul1  13951  binom3  14251  bernneq  14256  expmulnbnd  14262  discr  14267  bcm1k  14342  bcp1n  14343  reccn2  15638  binomlem  15873  binomfallfaclem2  16084  tanadd  16213  eirrlem  16250  dvds2ln  16337  bezoutlem4  16590  divgcdcoprm0  16713  modprm0  16855  nrginvrcnlem  24809  tcphcphlem2  25356  csbren  25519  radcnvlem1  26534  tanarg  26742  cxpeq  26880  quad2  26962  binom4  26973  dquartlem2  26975  dquart  26976  quart1lem  26978  dvatan  27058  log2cnv  27067  basellem8  27210  bcmono  27399  gausslemma2d  27496  lgsquadlem1  27502  2lgslem3b  27519  2lgslem3c  27520  2lgslem3d  27521  rplogsumlem1  27606  dchrisumlem2  27612  chpdifbndlem1  27675  selberg3lem1  27679  selberg4  27683  selberg3r  27691  pntrlog2bndlem2  27700  pntrlog2bndlem3  27701  pntrlog2bndlem5  27703  pntlemf  27727  pntlemo  27729  ostth2lem1  27740  ostth2lem3  27757  zringfrac  33761  constrrtcc  34042  logdivsqrle  34954  circum  36037  lcmineqlem8  42665  lcmineqlem12  42669  flt4lem5f  43251  jm2.25  43588  jm2.27c  43596  binomcxplemnotnn0  44930  dvasinbx  46492  stirlinglem3  46648  dirkercncflem2  46676  cevathlem1  47439  itschlc0yqe  49391