MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mul12d Unicode version

Theorem mul12d 9231
Description: Commutative/associative law that swaps the first two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
muld.1  |-  ( ph  ->  A  e.  CC )
addcomd.2  |-  ( ph  ->  B  e.  CC )
addcand.3  |-  ( ph  ->  C  e.  CC )
Assertion
Ref Expression
mul12d  |-  ( ph  ->  ( A  x.  ( B  x.  C )
)  =  ( B  x.  ( A  x.  C ) ) )

Proof of Theorem mul12d
StepHypRef Expression
1 muld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addcomd.2 . 2  |-  ( ph  ->  B  e.  CC )
3 addcand.3 . 2  |-  ( ph  ->  C  e.  CC )
4 mul12 9188 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  x.  C ) )  =  ( B  x.  ( A  x.  C )
) )
51, 2, 3, 4syl3anc 1184 1  |-  ( ph  ->  ( A  x.  ( B  x.  C )
)  =  ( B  x.  ( A  x.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721  (class class class)co 6040   CCcc 8944    x. cmul 8951
This theorem is referenced by:  divrec  9650  remullem  11888  sqreulem  12118  cvgrat  12615  tanval3  12690  sinadd  12720  dvdsmulgcd  13009  prmdiv  13129  vdwlem6  13309  itgmulc2  19678  dvexp3  19815  aaliou3lem8  20215  dvradcnv  20290  pserdvlem2  20297  abelthlem6  20305  abelthlem7  20307  tangtx  20366  tanarg  20467  dvcxp1  20579  dcubic1  20638  mcubic  20640  dquart  20646  quart1  20649  quartlem1  20650  asinsin  20685  basellem3  20818  bcp1ctr  21016  lgseisenlem2  21087  lgseisenlem4  21089  lgsquadlem1  21091  2sqlem4  21104  chebbnd1lem3  21118  rpvmasum2  21159  mulog2sumlem3  21183  selberglem1  21192  selberg4lem1  21207  selberg3r  21216  selberg34r  21218  pntrlog2bndlem4  21227  pntrlog2bndlem6  21230  pntlemr  21249  pntlemk  21253  ostth2lem3  21282  branmfn  23561  lgamgulmlem2  24767  binomrisefac  25309  faclimlem1  25310  colinearalglem4  25752  itgmulc2nc  26172  areacirclem2  26181  pellexlem6  26787  pell1234qrmulcl  26808  rmxyadd  26874  jm2.18  26949  jm2.19lem1  26950  jm2.22  26956  jm2.20nn  26958  proot1ex  27388  ofmul12  27410  stoweidlem11  27627  wallispi2lem1  27687  stirlinglem1  27690  stirlinglem3  27692  stirlinglem7  27696  stirlinglem15  27704
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-mulcom 9010  ax-mulass 9012
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043
  Copyright terms: Public domain W3C validator