Theorem mul32d 11354

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034   · cmul 11041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-mulcom 11100  ax-mulass 11102

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366

This theorem is referenced by:  conjmul  11870  modmul1  13884  binom3  14184  bernneq  14189  expmulnbnd  14195  discr  14200  bcm1k  14275  bcp1n  14276  reccn2  15557  binomlem  15792  binomfallfaclem2  16003  tanadd  16132  eirrlem  16169  dvds2ln  16256  bezoutlem4  16509  divgcdcoprm0  16632  modprm0  16774  nrginvrcnlem  24681  tcphcphlem2  25228  csbren  25391  radcnvlem1  26403  tanarg  26608  cxpeq  26746  quad2  26828  binom4  26839  dquartlem2  26841  dquart  26842  quart1lem  26844  dvatan  26924  log2cnv  26933  basellem8  27076  bcmono  27265  gausslemma2d  27362  lgsquadlem1  27368  2lgslem3b  27385  2lgslem3c  27386  2lgslem3d  27387  rplogsumlem1  27472  dchrisumlem2  27478  chpdifbndlem1  27541  selberg3lem1  27545  selberg4  27549  selberg3r  27557  pntrlog2bndlem2  27566  pntrlog2bndlem3  27567  pntrlog2bndlem5  27569  pntlemf  27593  pntlemo  27595  ostth2lem1  27606  ostth2lem3  27623  zringfrac  33644  constrrtcc  33926  logdivsqrle  34841  circum  35909  lcmineqlem8  42528  lcmineqlem12  42532  flt4lem5f  43114  jm2.25  43451  jm2.27c  43459  binomcxplemnotnn0  44807  dvasinbx  46370  stirlinglem3  46526  dirkercncflem2  46554  cevathlem1  47317  itschlc0yqe  49258