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

Theorem mul12d 9822
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 9779 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  x.  C ) )  =  ( B  x.  ( A  x.  C )
) )
51, 2, 3, 4syl3anc 1230 1  |-  ( ph  ->  ( A  x.  ( B  x.  C )
)  =  ( B  x.  ( A  x.  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1405    e. wcel 1842  (class class class)co 6277   CCcc 9519    x. cmul 9526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-mulcom 9585  ax-mulass 9587
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-iota 5532  df-fv 5576  df-ov 6280
This theorem is referenced by:  divrec  10263  remullem  13108  sqreulem  13339  cvgrat  13842  binomrisefac  13985  tanval3  14076  sinadd  14106  dvdsmulgcd  14399  prmdiv  14522  vdwlem6  14711  itgmulc2  22530  dvexp3  22669  aaliou3lem8  23031  dvradcnv  23106  pserdvlem2  23113  abelthlem6  23121  abelthlem7  23123  tangtx  23188  tanarg  23296  dvcxp1  23408  dvcncxp1  23411  heron  23492  dcubic1  23499  mcubic  23501  dquart  23507  quart1  23510  quartlem1  23511  asinsin  23546  lgamgulmlem2  23683  basellem3  23735  bcp1ctr  23933  lgseisenlem2  24004  lgseisenlem4  24006  lgsquadlem1  24008  2sqlem4  24021  chebbnd1lem3  24035  rpvmasum2  24076  mulog2sumlem3  24100  selberglem1  24109  selberg4lem1  24124  selberg3r  24133  selberg34r  24135  pntrlog2bndlem4  24144  pntrlog2bndlem6  24147  pntlemr  24166  pntlemk  24170  ostth2lem3  24199  colinearalglem4  24616  branmfn  27423  faclimlem1  29939  itgmulc2nc  31436  areacirclem1  31458  pellexlem6  35111  pell1234qrmulcl  35132  rmxyadd  35198  jm2.18  35272  jm2.19lem1  35273  jm2.22  35279  jm2.20nn  35281  proot1ex  35505  lcmgcdlem  36040  ofmul12  36058  binomcxplemnotnn0  36089  sineq0ALT  36748  mul13d  36815  stoweidlem11  37142  wallispi2lem1  37202  stirlinglem1  37205  stirlinglem3  37207  stirlinglem7  37211  stirlinglem15  37219  dirkertrigeqlem3  37231  dirkercncflem2  37235  fourierdlem66  37304  fourierdlem83  37321  etransclem23  37389  2zlidl  38232
  Copyright terms: Public domain W3C validator