Theorem mul32d 11474

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  (class class class)co 7424  ℂcc 11156   · cmul 11163

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-mulcom 11222  ax-mulass 11224

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-iota 6506  df-fv 6562  df-ov 7427

This theorem is referenced by:  conjmul  11982  modmul1  13944  binom3  14241  bernneq  14246  expmulnbnd  14252  discr  14257  bcm1k  14332  bcp1n  14333  reccn2  15599  binomlem  15833  binomfallfaclem2  16042  tanadd  16169  eirrlem  16206  dvds2ln  16291  bezoutlem4  16543  divgcdcoprm0  16666  modprm0  16807  nrginvrcnlem  24699  tcphcphlem2  25255  csbren  25418  radcnvlem1  26442  tanarg  26646  cxpeq  26785  quad2  26867  binom4  26878  dquartlem2  26880  dquart  26881  quart1lem  26883  dvatan  26963  log2cnv  26972  basellem8  27116  bcmono  27306  gausslemma2d  27403  lgsquadlem1  27409  2lgslem3b  27426  2lgslem3c  27427  2lgslem3d  27428  rplogsumlem1  27513  dchrisumlem2  27519  chpdifbndlem1  27582  selberg3lem1  27586  selberg4  27590  selberg3r  27598  pntrlog2bndlem2  27607  pntrlog2bndlem3  27608  pntrlog2bndlem5  27610  pntlemf  27634  pntlemo  27636  ostth2lem1  27647  ostth2lem3  27664  zringfrac  33429  logdivsqrle  34496  circum  35502  lcmineqlem8  41735  lcmineqlem12  41739  flt4lem5f  42311  jm2.25  42657  jm2.27c  42665  binomcxplemnotnn0  44030  dvasinbx  45541  stirlinglem3  45697  dirkercncflem2  45725  cevathlem1  46488  itschlc0yqe  48148