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

Theorem mul32d 9575
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 9532 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( ( A  x.  C )  x.  B ) )
51, 2, 3, 4syl3anc 1213 1  |-  ( ph  ->  ( ( A  x.  B )  x.  C
)  =  ( ( A  x.  C )  x.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364    e. wcel 1761  (class class class)co 6090   CCcc 9276    x. cmul 9283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-mulcom 9342  ax-mulass 9344
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-iota 5378  df-fv 5423  df-ov 6093
This theorem is referenced by:  conjmul  10044  modmul1  11748  binom3  11981  bernneq  11986  expmulnbnd  11992  discr  11997  bcm1k  12087  bcp1n  12088  reccn2  13070  binomlem  13288  tanadd  13447  eirrlem  13482  dvds2ln  13559  bezoutlem4  13721  modprm0  13869  nrginvrcnlem  20230  tchcphlem2  20710  csbren  20857  radcnvlem1  21837  tanarg  22027  cxpeq  22154  quad2  22193  binom4  22204  dquartlem2  22206  dquart  22207  quart1lem  22209  dvatan  22289  log2cnv  22298  basellem8  22384  bcmono  22575  lgsquadlem1  22652  rplogsumlem1  22692  dchrisumlem2  22698  chpdifbndlem1  22761  selberg3lem1  22765  selberg4  22769  selberg3r  22777  pntrlog2bndlem2  22786  pntrlog2bndlem3  22787  pntrlog2bndlem5  22789  pntlemf  22813  pntlemo  22815  ostth2lem1  22826  ostth2lem3  22843  circum  27248  binomfallfaclem2  27472  jm2.25  29273  jm2.27c  29281  stirlinglem3  29796  cevathlem1  29828
  Copyright terms: Public domain W3C validator