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

Theorem mul12d 9565
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 9522 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  x.  C ) )  =  ( B  x.  ( A  x.  C )
) )
51, 2, 3, 4syl3anc 1211 1  |-  ( ph  ->  ( A  x.  ( B  x.  C )
)  =  ( B  x.  ( A  x.  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    e. wcel 1755  (class class class)co 6080   CCcc 9267    x. cmul 9274
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-mulcom 9333  ax-mulass 9335
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083
This theorem is referenced by:  divrec  9997  remullem  12600  sqreulem  12830  cvgrat  13325  tanval3  13400  sinadd  13430  dvdsmulgcd  13720  prmdiv  13842  vdwlem6  14029  itgmulc2  21152  dvexp3  21291  aaliou3lem8  21695  dvradcnv  21770  pserdvlem2  21777  abelthlem6  21785  abelthlem7  21787  tangtx  21851  tanarg  21952  dvcxp1  22064  heron  22117  dcubic1  22124  mcubic  22126  dquart  22132  quart1  22135  quartlem1  22136  asinsin  22171  basellem3  22304  bcp1ctr  22502  lgseisenlem2  22573  lgseisenlem4  22575  lgsquadlem1  22577  2sqlem4  22590  chebbnd1lem3  22604  rpvmasum2  22645  mulog2sumlem3  22669  selberglem1  22678  selberg4lem1  22693  selberg3r  22702  selberg34r  22704  pntrlog2bndlem4  22713  pntrlog2bndlem6  22716  pntlemr  22735  pntlemk  22739  ostth2lem3  22768  colinearalglem4  22977  branmfn  25331  lgamgulmlem2  26863  binomrisefac  27391  faclimlem1  27395  itgmulc2nc  28301  dvcncxp1  28318  areacirclem1  28325  pellexlem6  29017  pell1234qrmulcl  29038  rmxyadd  29104  jm2.18  29179  jm2.19lem1  29180  jm2.22  29186  jm2.20nn  29188  proot1ex  29411  ofmul12  29441  stoweidlem11  29649  wallispi2lem1  29709  stirlinglem1  29712  stirlinglem3  29714  stirlinglem7  29718  stirlinglem15  29726  sineq0ALT  31372
  Copyright terms: Public domain W3C validator