Theorem mul32d 11384

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   · cmul 11073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-mulcom 11132  ax-mulass 11134

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  conjmul  11899  modmul1  13889  binom3  14189  bernneq  14194  expmulnbnd  14200  discr  14205  bcm1k  14280  bcp1n  14281  reccn2  15563  binomlem  15795  binomfallfaclem2  16006  tanadd  16135  eirrlem  16172  dvds2ln  16259  bezoutlem4  16512  divgcdcoprm0  16635  modprm0  16776  nrginvrcnlem  24579  tcphcphlem2  25136  csbren  25299  radcnvlem1  26322  tanarg  26528  cxpeq  26667  quad2  26749  binom4  26760  dquartlem2  26762  dquart  26763  quart1lem  26765  dvatan  26845  log2cnv  26854  basellem8  26998  bcmono  27188  gausslemma2d  27285  lgsquadlem1  27291  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  rplogsumlem1  27395  dchrisumlem2  27401  chpdifbndlem1  27464  selberg3lem1  27468  selberg4  27472  selberg3r  27480  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem5  27492  pntlemf  27516  pntlemo  27518  ostth2lem1  27529  ostth2lem3  27546  zringfrac  33525  constrrtcc  33725  logdivsqrle  34641  circum  35661  lcmineqlem8  42024  lcmineqlem12  42028  flt4lem5f  42645  jm2.25  42988  jm2.27c  42996  binomcxplemnotnn0  44345  dvasinbx  45918  stirlinglem3  46074  dirkercncflem2  46102  cevathlem1  46865  itschlc0yqe  48749