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

Theorem mul12d 9275
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 9232 . 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 1652    e. wcel 1725  (class class class)co 6081   CCcc 8988    x. cmul 8995
This theorem is referenced by:  divrec  9694  remullem  11933  sqreulem  12163  cvgrat  12660  tanval3  12735  sinadd  12765  dvdsmulgcd  13054  prmdiv  13174  vdwlem6  13354  itgmulc2  19725  dvexp3  19862  aaliou3lem8  20262  dvradcnv  20337  pserdvlem2  20344  abelthlem6  20352  abelthlem7  20354  tangtx  20413  tanarg  20514  dvcxp1  20626  dcubic1  20685  mcubic  20687  dquart  20693  quart1  20696  quartlem1  20697  asinsin  20732  basellem3  20865  bcp1ctr  21063  lgseisenlem2  21134  lgseisenlem4  21136  lgsquadlem1  21138  2sqlem4  21151  chebbnd1lem3  21165  rpvmasum2  21206  mulog2sumlem3  21230  selberglem1  21239  selberg4lem1  21254  selberg3r  21263  selberg34r  21265  pntrlog2bndlem4  21274  pntrlog2bndlem6  21277  pntlemr  21296  pntlemk  21300  ostth2lem3  21329  branmfn  23608  lgamgulmlem2  24814  binomrisefac  25358  faclimlem1  25362  colinearalglem4  25848  itgmulc2nc  26273  areacirclem1  26292  pellexlem6  26897  pell1234qrmulcl  26918  rmxyadd  26984  jm2.18  27059  jm2.19lem1  27060  jm2.22  27066  jm2.20nn  27068  proot1ex  27497  ofmul12  27519  stoweidlem11  27736  wallispi2lem1  27796  stirlinglem1  27799  stirlinglem3  27801  stirlinglem7  27805  stirlinglem15  27813  sineq0ALT  29049
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-mulcom 9054  ax-mulass 9056
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rex 2711  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-iota 5418  df-fv 5462  df-ov 6084
  Copyright terms: Public domain W3C validator