Theorem mul32d 10881

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2112  (class class class)co 7151  ℂcc 10566   · cmul 10573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730  ax-mulcom 10632  ax-mulass 10634

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-un 3864  df-in 3866  df-ss 3876  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-iota 6295  df-fv 6344  df-ov 7154

This theorem is referenced by:  conjmul  11388  modmul1  13334  binom3  13628  bernneq  13633  expmulnbnd  13639  discr  13644  bcm1k  13718  bcp1n  13719  reccn2  14994  binomlem  15225  binomfallfaclem2  15435  tanadd  15561  eirrlem  15598  dvds2ln  15683  bezoutlem4  15934  divgcdcoprm0  16054  modprm0  16190  nrginvrcnlem  23386  tcphcphlem2  23929  csbren  24092  radcnvlem1  25100  tanarg  25302  cxpeq  25438  quad2  25517  binom4  25528  dquartlem2  25530  dquart  25531  quart1lem  25533  dvatan  25613  log2cnv  25622  basellem8  25765  bcmono  25953  gausslemma2d  26050  lgsquadlem1  26056  2lgslem3b  26073  2lgslem3c  26074  2lgslem3d  26075  rplogsumlem1  26160  dchrisumlem2  26166  chpdifbndlem1  26229  selberg3lem1  26233  selberg4  26237  selberg3r  26245  pntrlog2bndlem2  26254  pntrlog2bndlem3  26255  pntrlog2bndlem5  26257  pntlemf  26281  pntlemo  26283  ostth2lem1  26294  ostth2lem3  26311  logdivsqrle  32142  circum  33141  lcmineqlem8  39596  lcmineqlem12  39600  flt4lem5f  39979  jm2.25  40306  jm2.27c  40314  binomcxplemnotnn0  41426  dvasinbx  42921  stirlinglem3  43077  dirkercncflem2  43105  cevathlem1  43840  itschlc0yqe  45532