Theorem mul32d 11448

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7417  ℂcc 11126   · cmul 11133

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-mulcom 11192  ax-mulass 11194

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420

This theorem is used by:  conjmul  11960  modmul1  13992  binom3  14292  bernneq  14297  expmulnbnd  14303  discr  14308  bcm1k  14383  bcp1n  14384  reccn2  15688  binomlem  15922  binomfallfaclem2  16132  tanadd  16261  eirrlem  16298  dvds2ln  16385  bezoutlem4  16638  divgcdcoprm0  16761  modprm0  16903  nrginvrcnlem  24923  tcphcphlem2  25470  csbren  25633  radcnvlem1  26656  tanarg  26864  cxpeq  27002  quad2  27084  binom4  27095  dquartlem2  27097  dquart  27098  quart1lem  27100  dvatan  27180  log2cnv  27189  basellem8  27332  bcmono  27521  gausslemma2d  27618  lgsquadlem1  27624  2lgslem3b  27641  2lgslem3c  27642  2lgslem3d  27643  rplogsumlem1  27728  dchrisumlem2  27734  chpdifbndlem1  27797  selberg3lem1  27801  selberg4  27805  selberg3r  27813  pntrlog2bndlem2  27822  pntrlog2bndlem3  27823  pntrlog2bndlem5  27825  pntlemf  27849  pntlemo  27851  ostth2lem1  27862  ostth2lem3  27879  zringfrac  33972  constrrtcc  34253  logdivsqrle  35166  circum  36261  lcmineqlem8  42910  lcmineqlem12  42914  flt4lem5f  43511  jm2.25  43848  jm2.27c  43856  binomcxplemnotnn0  45188  dvasinbx  46756  stirlinglem3  46912  dirkercncflem2  46940  cevathlem1  47703  itschlc0yqe  49698