Theorem mul32d 11523

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201   · cmul 11208

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-mulcom 11267  ax-mulass 11269

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  conjmul  12037  modmul1  14070  binom3  14371  bernneq  14376  expmulnbnd  14382  discr  14387  bcm1k  14462  bcp1n  14463  reccn2  15769  binomlem  16003  binomfallfaclem2  16211  tanadd  16340  eirrlem  16377  dvds2ln  16464  bezoutlem4  16720  divgcdcoprm0  16845  modprm0  16988  nrginvrcnlem  25015  tcphcphlem2  25562  csbren  25725  radcnvlem1  26745  tanarg  26952  cxpeq  27090  quad2  27172  binom4  27183  dquartlem2  27185  dquart  27186  quart1lem  27188  dvatan  27268  log2cnv  27277  basellem8  27420  bcmono  27609  gausslemma2d  27706  lgsquadlem1  27712  2lgslem3b  27729  2lgslem3c  27730  2lgslem3d  27731  rplogsumlem1  27816  dchrisumlem2  27822  chpdifbndlem1  27885  selberg3lem1  27889  selberg4  27893  selberg3r  27901  pntrlog2bndlem2  27910  pntrlog2bndlem3  27911  pntrlog2bndlem5  27913  pntlemf  27937  pntlemo  27939  ostth2lem1  27950  ostth2lem3  27967  flt4lem5f  27992  zringfrac  34132  constrrtcc  34413  logdivsqrle  35325  circum  36525  lcmineqlem8  43179  lcmineqlem12  43183  jm2.25  44099  jm2.27c  44107  binomcxplemnotnn0  45433  dvasinbx  47023  stirlinglem3  47179  dirkercncflem2  47207  cevathlem1  47970  itschlc0yqe  49965