Theorem mul32d 10536

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

Syntax hints:   → wi 4   = wceq 1653   ∈ wcel 2157  (class class class)co 6878  ℂcc 10222   · cmul 10229

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-mulcom 10288  ax-mulass 10290

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-rex 3095  df-rab 3098  df-v 3387  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4844  df-iota 6064  df-fv 6109  df-ov 6881

This theorem is referenced by:  conjmul  11034  modmul1  12978  binom3  13239  bernneq  13244  expmulnbnd  13250  discr  13255  bcm1k  13355  bcp1n  13356  reccn2  14668  binomlem  14899  binomfallfaclem2  15107  tanadd  15233  eirrlem  15268  dvds2ln  15353  bezoutlem4  15594  divgcdcoprm0  15713  modprm0  15843  nrginvrcnlem  22823  tcphcphlem2  23362  csbren  23521  radcnvlem1  24508  tanarg  24706  cxpeq  24842  quad2  24918  binom4  24929  dquartlem2  24931  dquart  24932  quart1lem  24934  dvatan  25014  log2cnv  25023  basellem8  25166  bcmono  25354  gausslemma2d  25451  lgsquadlem1  25457  2lgslem3b  25474  2lgslem3c  25475  2lgslem3d  25476  rplogsumlem1  25525  dchrisumlem2  25531  chpdifbndlem1  25594  selberg3lem1  25598  selberg4  25602  selberg3r  25610  pntrlog2bndlem2  25619  pntrlog2bndlem3  25620  pntrlog2bndlem5  25622  pntlemf  25646  pntlemo  25648  ostth2lem1  25659  ostth2lem3  25676  logdivsqrle  31248  circum  32083  jm2.25  38347  jm2.27c  38355  binomcxplemnotnn0  39333  dvasinbx  40875  stirlinglem3  41032  dirkercncflem2  41060  cevathlem1  41798