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

Theorem mul32d 9788
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 9745 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( ( A  x.  C )  x.  B ) )
51, 2, 3, 4syl3anc 1228 1  |-  ( ph  ->  ( ( A  x.  B )  x.  C
)  =  ( ( A  x.  C )  x.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767  (class class class)co 6283   CCcc 9489    x. cmul 9496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-mulcom 9555  ax-mulass 9557
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5550  df-fv 5595  df-ov 6286
This theorem is referenced by:  conjmul  10260  modmul1  12007  binom3  12254  bernneq  12259  expmulnbnd  12265  discr  12270  bcm1k  12360  bcp1n  12361  reccn2  13381  binomlem  13603  tanadd  13762  eirrlem  13797  dvds2ln  13874  bezoutlem4  14037  modprm0  14188  nrginvrcnlem  20950  tchcphlem2  21430  csbren  21577  radcnvlem1  22558  tanarg  22748  cxpeq  22875  quad2  22914  binom4  22925  dquartlem2  22927  dquart  22928  quart1lem  22930  dvatan  23010  log2cnv  23019  basellem8  23105  bcmono  23296  lgsquadlem1  23373  rplogsumlem1  23413  dchrisumlem2  23419  chpdifbndlem1  23482  selberg3lem1  23486  selberg4  23490  selberg3r  23498  pntrlog2bndlem2  23507  pntrlog2bndlem3  23508  pntrlog2bndlem5  23510  pntlemf  23534  pntlemo  23536  ostth2lem1  23547  ostth2lem3  23564  circum  28531  binomfallfaclem2  28755  jm2.25  30561  jm2.27c  30569  dvasinbx  31266  stirlinglem3  31392  dirkercncflem2  31420  cevathlem1  31567
  Copyright terms: Public domain W3C validator