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

Theorem mul32d 11299
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 11255 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵))
51, 2, 3, 4syl3anc 1372 1 (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  (class class class)co 7350  cc 10983   · cmul 10990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709  ax-mulcom 11049  ax-mulass 11051
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-iota 6444  df-fv 6500  df-ov 7353
This theorem is referenced by:  conjmul  11806  modmul1  13759  binom3  14054  bernneq  14059  expmulnbnd  14065  discr  14070  bcm1k  14144  bcp1n  14145  reccn2  15415  binomlem  15650  binomfallfaclem2  15859  tanadd  15985  eirrlem  16022  dvds2ln  16107  bezoutlem4  16359  divgcdcoprm0  16477  modprm0  16613  nrginvrcnlem  23983  tcphcphlem2  24528  csbren  24691  radcnvlem1  25700  tanarg  25902  cxpeq  26038  quad2  26117  binom4  26128  dquartlem2  26130  dquart  26131  quart1lem  26133  dvatan  26213  log2cnv  26222  basellem8  26365  bcmono  26553  gausslemma2d  26650  lgsquadlem1  26656  2lgslem3b  26673  2lgslem3c  26674  2lgslem3d  26675  rplogsumlem1  26760  dchrisumlem2  26766  chpdifbndlem1  26829  selberg3lem1  26833  selberg4  26837  selberg3r  26845  pntrlog2bndlem2  26854  pntrlog2bndlem3  26855  pntrlog2bndlem5  26857  pntlemf  26881  pntlemo  26883  ostth2lem1  26894  ostth2lem3  26911  logdivsqrle  33043  circum  34044  lcmineqlem8  40424  lcmineqlem12  40428  flt4lem5f  40897  jm2.25  41225  jm2.27c  41233  binomcxplemnotnn0  42437  dvasinbx  43952  stirlinglem3  44108  dirkercncflem2  44136  cevathlem1  44899  itschlc0yqe  46637
  Copyright terms: Public domain W3C validator