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

Theorem mul4d 9844
Description: Rearrangement of 4 factors. (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 )
mul4d.4  |-  ( ph  ->  D  e.  CC )
Assertion
Ref Expression
mul4d  |-  ( ph  ->  ( ( A  x.  B )  x.  ( C  x.  D )
)  =  ( ( A  x.  C )  x.  ( B  x.  D ) ) )

Proof of Theorem mul4d
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 mul4d.4 . 2  |-  ( ph  ->  D  e.  CC )
5 mul4 9801 . 2  |-  ( ( ( A  e.  CC  /\  B  e.  CC )  /\  ( C  e.  CC  /\  D  e.  CC ) )  -> 
( ( A  x.  B )  x.  ( C  x.  D )
)  =  ( ( A  x.  C )  x.  ( B  x.  D ) ) )
61, 2, 3, 4, 5syl22anc 1265 1  |-  ( ph  ->  ( ( A  x.  B )  x.  ( C  x.  D )
)  =  ( ( A  x.  C )  x.  ( B  x.  D ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1870  (class class class)co 6305   CCcc 9536    x. cmul 9543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-mulcl 9600  ax-mulcom 9602  ax-mulass 9604
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308
This theorem is referenced by:  remullem  13170  absmul  13336  binomrisefac  14073  cosadd  14197  tanadd  14199  eulerthlem2  14699  mul4sqlem  14860  odadd2  17426  itgmulc2  22676  plymullem1  23044  chordthmlem4  23634  heron  23637  quartlem1  23656  dchrmulcl  24048  bposlem9  24091  lgsdir  24129  lgsdi  24131  lgsquad2lem1  24157  chtppilimlem1  24182  rplogsumlem1  24193  dchrvmasumlem1  24204  dchrvmasum2lem  24205  chpdifbndlem1  24262  pntlemf  24314  brbtwn2  24789  colinearalglem4  24793  madjusmdetlem4  28503  circum  30114  itgmulc2nc  31725  pellexlem6  35399  pell1234qrmulcl  35422  rmxyadd  35490  wallispi2lem2  37518  dirkertrigeqlem3  37546  cevathlem1  37891
  Copyright terms: Public domain W3C validator