Theorem mul32d 11347

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027   · cmul 11034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-mulcom 11093  ax-mulass 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363

This theorem is referenced by:  conjmul  11863  modmul1  13877  binom3  14177  bernneq  14182  expmulnbnd  14188  discr  14193  bcm1k  14268  bcp1n  14269  reccn2  15550  binomlem  15785  binomfallfaclem2  15996  tanadd  16125  eirrlem  16162  dvds2ln  16249  bezoutlem4  16502  divgcdcoprm0  16625  modprm0  16767  nrginvrcnlem  24666  tcphcphlem2  25213  csbren  25376  radcnvlem1  26391  tanarg  26596  cxpeq  26734  quad2  26816  binom4  26827  dquartlem2  26829  dquart  26830  quart1lem  26832  dvatan  26912  log2cnv  26921  basellem8  27065  bcmono  27254  gausslemma2d  27351  lgsquadlem1  27357  2lgslem3b  27374  2lgslem3c  27375  2lgslem3d  27376  rplogsumlem1  27461  dchrisumlem2  27467  chpdifbndlem1  27530  selberg3lem1  27534  selberg4  27538  selberg3r  27546  pntrlog2bndlem2  27555  pntrlog2bndlem3  27556  pntrlog2bndlem5  27558  pntlemf  27582  pntlemo  27584  ostth2lem1  27595  ostth2lem3  27612  zringfrac  33629  constrrtcc  33895  logdivsqrle  34810  circum  35872  lcmineqlem8  42489  lcmineqlem12  42493  flt4lem5f  43104  jm2.25  43445  jm2.27c  43453  binomcxplemnotnn0  44801  dvasinbx  46366  stirlinglem3  46522  dirkercncflem2  46550  cevathlem1  47313  itschlc0yqe  49248