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

Theorem mul32d 11366
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 11322 . 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 7358  โ„‚cc 11050   ยท cmul 11057
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 2708  ax-mulcom 11116  ax-mulass 11118
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 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361
This theorem is referenced by:  conjmul  11873  modmul1  13830  binom3  14128  bernneq  14133  expmulnbnd  14139  discr  14144  bcm1k  14216  bcp1n  14217  reccn2  15480  binomlem  15715  binomfallfaclem2  15924  tanadd  16050  eirrlem  16087  dvds2ln  16172  bezoutlem4  16424  divgcdcoprm0  16542  modprm0  16678  nrginvrcnlem  24058  tcphcphlem2  24603  csbren  24766  radcnvlem1  25775  tanarg  25977  cxpeq  26113  quad2  26192  binom4  26203  dquartlem2  26205  dquart  26206  quart1lem  26208  dvatan  26288  log2cnv  26297  basellem8  26440  bcmono  26628  gausslemma2d  26725  lgsquadlem1  26731  2lgslem3b  26748  2lgslem3c  26749  2lgslem3d  26750  rplogsumlem1  26835  dchrisumlem2  26841  chpdifbndlem1  26904  selberg3lem1  26908  selberg4  26912  selberg3r  26920  pntrlog2bndlem2  26929  pntrlog2bndlem3  26930  pntrlog2bndlem5  26932  pntlemf  26956  pntlemo  26958  ostth2lem1  26969  ostth2lem3  26986  logdivsqrle  33266  circum  34265  lcmineqlem8  40496  lcmineqlem12  40500  flt4lem5f  40998  jm2.25  41326  jm2.27c  41334  binomcxplemnotnn0  42643  dvasinbx  44168  stirlinglem3  44324  dirkercncflem2  44352  cevathlem1  45115  itschlc0yqe  46853
  Copyright terms: Public domain W3C validator