Theorem mul32d 10850

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535   · cmul 10542

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-mulcom 10601  ax-mulass 10603

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159

This theorem is referenced by:  conjmul  11357  modmul1  13293  binom3  13586  bernneq  13591  expmulnbnd  13597  discr  13602  bcm1k  13676  bcp1n  13677  reccn2  14953  binomlem  15184  binomfallfaclem2  15394  tanadd  15520  eirrlem  15557  dvds2ln  15642  bezoutlem4  15890  divgcdcoprm0  16009  modprm0  16142  nrginvrcnlem  23300  tcphcphlem2  23839  csbren  24002  radcnvlem1  25001  tanarg  25202  cxpeq  25338  quad2  25417  binom4  25428  dquartlem2  25430  dquart  25431  quart1lem  25433  dvatan  25513  log2cnv  25522  basellem8  25665  bcmono  25853  gausslemma2d  25950  lgsquadlem1  25956  2lgslem3b  25973  2lgslem3c  25974  2lgslem3d  25975  rplogsumlem1  26060  dchrisumlem2  26066  chpdifbndlem1  26129  selberg3lem1  26133  selberg4  26137  selberg3r  26145  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem5  26157  pntlemf  26181  pntlemo  26183  ostth2lem1  26194  ostth2lem3  26211  logdivsqrle  31921  circum  32917  jm2.25  39616  jm2.27c  39624  binomcxplemnotnn0  40708  dvasinbx  42225  stirlinglem3  42381  dirkercncflem2  42409  cevathlem1  43144  itschlc0yqe  44767