MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mul32d Structured version   Visualization version   GIF version

Theorem mul32d 10093
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
StepHypRef Expression
1 muld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcomd.2 . 2 (𝜑𝐵 ∈ ℂ)
3 addcand.3 . 2 (𝜑𝐶 ∈ ℂ)
4 mul32 10050 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵))
51, 2, 3, 4syl3anc 1317 1 (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1975  (class class class)co 6523  cc 9786   · cmul 9793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-mulcom 9852  ax-mulass 9854
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-rex 2897  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-br 4574  df-iota 5750  df-fv 5794  df-ov 6526
This theorem is referenced by:  conjmul  10587  modmul1  12536  binom3  12798  bernneq  12803  expmulnbnd  12809  discr  12814  bcm1k  12915  bcp1n  12916  reccn2  14117  binomlem  14342  binomfallfaclem2  14552  tanadd  14678  eirrlem  14713  dvds2ln  14794  bezoutlem4  15039  divgcdcoprm0  15159  modprm0  15290  nrginvrcnlem  22234  tchcphlem2  22760  csbren  22903  radcnvlem1  23884  tanarg  24082  cxpeq  24211  quad2  24279  binom4  24290  dquartlem2  24292  dquart  24293  quart1lem  24295  dvatan  24375  log2cnv  24384  basellem8  24527  bcmono  24715  gausslemma2d  24812  lgsquadlem1  24818  2lgslem3b  24835  2lgslem3c  24836  2lgslem3d  24837  rplogsumlem1  24886  dchrisumlem2  24892  chpdifbndlem1  24955  selberg3lem1  24959  selberg4  24963  selberg3r  24971  pntrlog2bndlem2  24980  pntrlog2bndlem3  24981  pntrlog2bndlem5  24983  pntlemf  25007  pntlemo  25009  ostth2lem1  25020  ostth2lem3  25037  circum  30624  jm2.25  36383  jm2.27c  36391  binomcxplemnotnn0  37376  dvasinbx  38610  stirlinglem3  38769  dirkercncflem2  38797  cevathlem1  39505
  Copyright terms: Public domain W3C validator