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

Theorem mul32d 9278
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 9235 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( ( A  x.  C )  x.  B ) )
51, 2, 3, 4syl3anc 1185 1  |-  ( ph  ->  ( ( A  x.  B )  x.  C
)  =  ( ( A  x.  C )  x.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726  (class class class)co 6083   CCcc 8990    x. cmul 8997
This theorem is referenced by:  conjmul  9733  modmul1  11281  binom3  11502  bernneq  11507  expmulnbnd  11513  discr  11518  bcm1k  11608  bcp1n  11609  reccn2  12392  binomlem  12610  tanadd  12770  eirrlem  12805  dvds2ln  12882  bezoutlem4  13043  nrginvrcnlem  18728  tchcphlem2  19195  radcnvlem1  20331  tanarg  20516  cxpeq  20643  quad2  20681  binom4  20692  dquartlem2  20694  dquart  20695  quart1lem  20697  dvatan  20777  log2cnv  20786  basellem8  20872  bcmono  21063  lgsquadlem1  21140  rplogsumlem1  21180  dchrisumlem2  21186  chpdifbndlem1  21249  selberg3lem1  21253  selberg4  21257  selberg3r  21265  pntrlog2bndlem2  21274  pntrlog2bndlem3  21275  pntrlog2bndlem5  21277  pntlemf  21301  pntlemo  21303  ostth2lem1  21314  ostth2lem3  21331  circum  25113  binomfallfaclem2  25358  csbrn  26458  jm2.25  27072  jm2.27c  27080  stirlinglem3  27803  cevathlem1  27835  modprm0  28250
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-mulcom 9056  ax-mulass 9058
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-iota 5420  df-fv 5464  df-ov 6086
  Copyright terms: Public domain W3C validator