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

Theorem mul12d 9570
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 9527 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  x.  C ) )  =  ( B  x.  ( A  x.  C )
) )
51, 2, 3, 4syl3anc 1218 1  |-  ( ph  ->  ( A  x.  ( B  x.  C )
)  =  ( B  x.  ( A  x.  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756  (class class class)co 6086   CCcc 9272    x. cmul 9279
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-mulcom 9338  ax-mulass 9340
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089
This theorem is referenced by:  divrec  10002  remullem  12609  sqreulem  12839  cvgrat  13335  tanval3  13410  sinadd  13440  dvdsmulgcd  13730  prmdiv  13852  vdwlem6  14039  itgmulc2  21286  dvexp3  21425  aaliou3lem8  21786  dvradcnv  21861  pserdvlem2  21868  abelthlem6  21876  abelthlem7  21878  tangtx  21942  tanarg  22043  dvcxp1  22155  heron  22208  dcubic1  22215  mcubic  22217  dquart  22223  quart1  22226  quartlem1  22227  asinsin  22262  basellem3  22395  bcp1ctr  22593  lgseisenlem2  22664  lgseisenlem4  22666  lgsquadlem1  22668  2sqlem4  22681  chebbnd1lem3  22695  rpvmasum2  22736  mulog2sumlem3  22760  selberglem1  22769  selberg4lem1  22784  selberg3r  22793  selberg34r  22795  pntrlog2bndlem4  22804  pntrlog2bndlem6  22807  pntlemr  22826  pntlemk  22830  ostth2lem3  22859  colinearalglem4  23106  branmfn  25460  lgamgulmlem2  26968  binomrisefac  27496  faclimlem1  27500  itgmulc2nc  28413  dvcncxp1  28430  areacirclem1  28437  pellexlem6  29128  pell1234qrmulcl  29149  rmxyadd  29215  jm2.18  29290  jm2.19lem1  29291  jm2.22  29297  jm2.20nn  29299  proot1ex  29522  ofmul12  29552  stoweidlem11  29759  wallispi2lem1  29819  stirlinglem1  29822  stirlinglem3  29824  stirlinglem7  29828  stirlinglem15  29836  sineq0ALT  31560
  Copyright terms: Public domain W3C validator