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

Theorem mul12d 9682
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 9639 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  x.  C ) )  =  ( B  x.  ( A  x.  C )
) )
51, 2, 3, 4syl3anc 1219 1  |-  ( ph  ->  ( A  x.  ( B  x.  C )
)  =  ( B  x.  ( A  x.  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758  (class class class)co 6193   CCcc 9384    x. cmul 9391
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-mulcom 9450  ax-mulass 9452
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rex 2801  df-rab 2804  df-v 3073  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-br 4394  df-iota 5482  df-fv 5527  df-ov 6196
This theorem is referenced by:  divrec  10114  remullem  12728  sqreulem  12958  cvgrat  13454  tanval3  13529  sinadd  13559  dvdsmulgcd  13849  prmdiv  13971  vdwlem6  14158  itgmulc2  21437  dvexp3  21576  aaliou3lem8  21937  dvradcnv  22012  pserdvlem2  22019  abelthlem6  22027  abelthlem7  22029  tangtx  22093  tanarg  22194  dvcxp1  22306  heron  22359  dcubic1  22366  mcubic  22368  dquart  22374  quart1  22377  quartlem1  22378  asinsin  22413  basellem3  22546  bcp1ctr  22744  lgseisenlem2  22815  lgseisenlem4  22817  lgsquadlem1  22819  2sqlem4  22832  chebbnd1lem3  22846  rpvmasum2  22887  mulog2sumlem3  22911  selberglem1  22920  selberg4lem1  22935  selberg3r  22944  selberg34r  22946  pntrlog2bndlem4  22955  pntrlog2bndlem6  22958  pntlemr  22977  pntlemk  22981  ostth2lem3  23010  colinearalglem4  23300  branmfn  25654  lgamgulmlem2  27153  binomrisefac  27682  faclimlem1  27686  itgmulc2nc  28601  dvcncxp1  28618  areacirclem1  28625  pellexlem6  29316  pell1234qrmulcl  29337  rmxyadd  29403  jm2.18  29478  jm2.19lem1  29479  jm2.22  29485  jm2.20nn  29487  proot1ex  29710  ofmul12  29740  stoweidlem11  29947  wallispi2lem1  30007  stirlinglem1  30010  stirlinglem3  30012  stirlinglem7  30016  stirlinglem15  30024  sineq0ALT  31976
  Copyright terms: Public domain W3C validator