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

Theorem mul32d 9022
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 8979 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( ( A  x.  C )  x.  B ) )
51, 2, 3, 4syl3anc 1182 1  |-  ( ph  ->  ( ( A  x.  B )  x.  C
)  =  ( ( A  x.  C )  x.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735    x. cmul 8742
This theorem is referenced by:  conjmul  9477  modmul1  11002  binom3  11222  bernneq  11227  expmulnbnd  11233  discr  11238  bcm1k  11327  bcp1n  11328  reccn2  12070  binomlem  12287  tanadd  12447  eirrlem  12482  dvds2ln  12559  bezoutlem4  12720  nrginvrcnlem  18201  tchcphlem2  18666  radcnvlem1  19789  tanarg  19970  cxpeq  20097  quad2  20135  binom4  20146  dquartlem2  20148  dquart  20149  quart1lem  20151  dvatan  20231  log2cnv  20240  basellem8  20325  bcmono  20516  lgsquadlem1  20593  rplogsumlem1  20633  dchrisumlem2  20639  chpdifbndlem1  20702  selberg3lem1  20706  selberg4  20710  selberg3r  20718  pntrlog2bndlem2  20727  pntrlog2bndlem3  20728  pntrlog2bndlem5  20730  pntlemf  20754  pntlemo  20756  ostth2lem1  20767  ostth2lem3  20784  circum  24007  csbrn  26462  jm2.25  27092  jm2.27c  27100  stirlinglem3  27825  cevathlem1  27857
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-mulcom 8801  ax-mulass 8803
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator