Theorem mul32d 11500

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   · cmul 11189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-mulcom 11248  ax-mulass 11250

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  conjmul  12011  modmul1  13975  binom3  14273  bernneq  14278  expmulnbnd  14284  discr  14289  bcm1k  14364  bcp1n  14365  reccn2  15643  binomlem  15877  binomfallfaclem2  16088  tanadd  16215  eirrlem  16252  dvds2ln  16337  bezoutlem4  16589  divgcdcoprm0  16712  modprm0  16852  nrginvrcnlem  24733  tcphcphlem2  25289  csbren  25452  radcnvlem1  26474  tanarg  26679  cxpeq  26818  quad2  26900  binom4  26911  dquartlem2  26913  dquart  26914  quart1lem  26916  dvatan  26996  log2cnv  27005  basellem8  27149  bcmono  27339  gausslemma2d  27436  lgsquadlem1  27442  2lgslem3b  27459  2lgslem3c  27460  2lgslem3d  27461  rplogsumlem1  27546  dchrisumlem2  27552  chpdifbndlem1  27615  selberg3lem1  27619  selberg4  27623  selberg3r  27631  pntrlog2bndlem2  27640  pntrlog2bndlem3  27641  pntrlog2bndlem5  27643  pntlemf  27667  pntlemo  27669  ostth2lem1  27680  ostth2lem3  27697  zringfrac  33547  constrrtcc  33726  logdivsqrle  34627  circum  35642  lcmineqlem8  41993  lcmineqlem12  41997  flt4lem5f  42612  jm2.25  42956  jm2.27c  42964  binomcxplemnotnn0  44325  dvasinbx  45841  stirlinglem3  45997  dirkercncflem2  46025  cevathlem1  46788  itschlc0yqe  48494