Theorem mul32d 11472

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  (class class class)co 7432  ℂcc 11154   · cmul 11161

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-mulcom 11220  ax-mulass 11222

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-iota 6513  df-fv 6568  df-ov 7435

This theorem is referenced by:  conjmul  11985  modmul1  13966  binom3  14264  bernneq  14269  expmulnbnd  14275  discr  14280  bcm1k  14355  bcp1n  14356  reccn2  15634  binomlem  15866  binomfallfaclem2  16077  tanadd  16204  eirrlem  16241  dvds2ln  16327  bezoutlem4  16580  divgcdcoprm0  16703  modprm0  16844  nrginvrcnlem  24713  tcphcphlem2  25271  csbren  25434  radcnvlem1  26457  tanarg  26662  cxpeq  26801  quad2  26883  binom4  26894  dquartlem2  26896  dquart  26897  quart1lem  26899  dvatan  26979  log2cnv  26988  basellem8  27132  bcmono  27322  gausslemma2d  27419  lgsquadlem1  27425  2lgslem3b  27442  2lgslem3c  27443  2lgslem3d  27444  rplogsumlem1  27529  dchrisumlem2  27535  chpdifbndlem1  27598  selberg3lem1  27602  selberg4  27606  selberg3r  27614  pntrlog2bndlem2  27623  pntrlog2bndlem3  27624  pntrlog2bndlem5  27626  pntlemf  27650  pntlemo  27652  ostth2lem1  27663  ostth2lem3  27680  zringfrac  33583  constrrtcc  33777  logdivsqrle  34666  circum  35680  lcmineqlem8  42038  lcmineqlem12  42042  flt4lem5f  42672  jm2.25  43016  jm2.27c  43024  binomcxplemnotnn0  44380  dvasinbx  45940  stirlinglem3  46096  dirkercncflem2  46124  cevathlem1  46887  itschlc0yqe  48686