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

Theorem mul12d 9784
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 9741 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  x.  C ) )  =  ( B  x.  ( A  x.  C )
) )
51, 2, 3, 4syl3anc 1228 1  |-  ( ph  ->  ( A  x.  ( B  x.  C )
)  =  ( B  x.  ( A  x.  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767  (class class class)co 6282   CCcc 9486    x. cmul 9493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-mulcom 9552  ax-mulass 9554
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5549  df-fv 5594  df-ov 6285
This theorem is referenced by:  divrec  10219  remullem  12920  sqreulem  13151  cvgrat  13651  tanval3  13726  sinadd  13756  dvdsmulgcd  14047  prmdiv  14170  vdwlem6  14359  itgmulc2  21975  dvexp3  22114  aaliou3lem8  22475  dvradcnv  22550  pserdvlem2  22557  abelthlem6  22565  abelthlem7  22567  tangtx  22631  tanarg  22732  dvcxp1  22844  heron  22897  dcubic1  22904  mcubic  22906  dquart  22912  quart1  22915  quartlem1  22916  asinsin  22951  basellem3  23084  bcp1ctr  23282  lgseisenlem2  23353  lgseisenlem4  23355  lgsquadlem1  23357  2sqlem4  23370  chebbnd1lem3  23384  rpvmasum2  23425  mulog2sumlem3  23449  selberglem1  23458  selberg4lem1  23473  selberg3r  23482  selberg34r  23484  pntrlog2bndlem4  23493  pntrlog2bndlem6  23496  pntlemr  23515  pntlemk  23519  ostth2lem3  23548  colinearalglem4  23888  branmfn  26700  lgamgulmlem2  28212  binomrisefac  28741  faclimlem1  28745  itgmulc2nc  29660  dvcncxp1  29677  areacirclem1  29684  pellexlem6  30374  pell1234qrmulcl  30395  rmxyadd  30461  jm2.18  30534  jm2.19lem1  30535  jm2.22  30541  jm2.20nn  30543  proot1ex  30766  lcmgcdlem  30812  ofmul12  30830  mul13d  31038  stoweidlem11  31311  wallispi2lem1  31371  stirlinglem1  31374  stirlinglem3  31376  stirlinglem7  31380  stirlinglem15  31388  dirkertrigeqlem3  31400  dirkercncflem2  31404  fourierdlem66  31473  fourierdlem83  31490  sineq0ALT  32817
  Copyright terms: Public domain W3C validator