Theorem mul32d 11185

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  (class class class)co 7275  ℂcc 10869   · cmul 10876

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-mulcom 10935  ax-mulass 10937

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278

This theorem is referenced by:  conjmul  11692  modmul1  13644  binom3  13939  bernneq  13944  expmulnbnd  13950  discr  13955  bcm1k  14029  bcp1n  14030  reccn2  15306  binomlem  15541  binomfallfaclem2  15750  tanadd  15876  eirrlem  15913  dvds2ln  15998  bezoutlem4  16250  divgcdcoprm0  16370  modprm0  16506  nrginvrcnlem  23855  tcphcphlem2  24400  csbren  24563  radcnvlem1  25572  tanarg  25774  cxpeq  25910  quad2  25989  binom4  26000  dquartlem2  26002  dquart  26003  quart1lem  26005  dvatan  26085  log2cnv  26094  basellem8  26237  bcmono  26425  gausslemma2d  26522  lgsquadlem1  26528  2lgslem3b  26545  2lgslem3c  26546  2lgslem3d  26547  rplogsumlem1  26632  dchrisumlem2  26638  chpdifbndlem1  26701  selberg3lem1  26705  selberg4  26709  selberg3r  26717  pntrlog2bndlem2  26726  pntrlog2bndlem3  26727  pntrlog2bndlem5  26729  pntlemf  26753  pntlemo  26755  ostth2lem1  26766  ostth2lem3  26783  logdivsqrle  32630  circum  33632  lcmineqlem8  40044  lcmineqlem12  40048  flt4lem5f  40494  jm2.25  40821  jm2.27c  40829  binomcxplemnotnn0  41974  dvasinbx  43461  stirlinglem3  43617  dirkercncflem2  43645  cevathlem1  44383  itschlc0yqe  46106