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

Theorem mul32d 9232
Description: Commutative/associative law that swaps the last 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
mul32d  |-  ( ph  ->  ( ( A  x.  B )  x.  C
)  =  ( ( A  x.  C )  x.  B ) )

Proof of Theorem mul32d
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 mul32 9189 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( ( A  x.  C )  x.  B ) )
51, 2, 3, 4syl3anc 1184 1  |-  ( ph  ->  ( ( A  x.  B )  x.  C
)  =  ( ( A  x.  C )  x.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721  (class class class)co 6040   CCcc 8944    x. cmul 8951
This theorem is referenced by:  conjmul  9687  modmul1  11234  binom3  11455  bernneq  11460  expmulnbnd  11466  discr  11471  bcm1k  11561  bcp1n  11562  reccn2  12345  binomlem  12563  tanadd  12723  eirrlem  12758  dvds2ln  12835  bezoutlem4  12996  nrginvrcnlem  18679  tchcphlem2  19146  radcnvlem1  20282  tanarg  20467  cxpeq  20594  quad2  20632  binom4  20643  dquartlem2  20645  dquart  20646  quart1lem  20648  dvatan  20728  log2cnv  20737  basellem8  20823  bcmono  21014  lgsquadlem1  21091  rplogsumlem1  21131  dchrisumlem2  21137  chpdifbndlem1  21200  selberg3lem1  21204  selberg4  21208  selberg3r  21216  pntrlog2bndlem2  21225  pntrlog2bndlem3  21226  pntrlog2bndlem5  21228  pntlemf  21252  pntlemo  21254  ostth2lem1  21265  ostth2lem3  21282  circum  25064  binomfallfaclem2  25307  csbrn  26346  jm2.25  26960  jm2.27c  26968  stirlinglem3  27692  cevathlem1  27724
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-mulcom 9010  ax-mulass 9012
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043
  Copyright terms: Public domain W3C validator