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

Theorem mul4d 9580
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 9537 . 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 1219 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 1369    e. wcel 1756  (class class class)co 6090   CCcc 9279    x. cmul 9286
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-mulcl 9343  ax-mulcom 9345  ax-mulass 9347
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-rex 2720  df-rab 2723  df-v 2973  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-nul 3637  df-if 3791  df-sn 3877  df-pr 3879  df-op 3883  df-uni 4091  df-br 4292  df-iota 5380  df-fv 5425  df-ov 6093
This theorem is referenced by:  remullem  12616  absmul  12782  cosadd  13448  tanadd  13450  eulerthlem2  13856  mul4sqlem  14013  odadd2  16330  itgmulc2  21310  plymullem1  21681  chordthmlem4  22229  heron  22232  quartlem1  22251  dchrmulcl  22587  bposlem9  22630  lgsdir  22668  lgsdi  22670  lgsquad2lem1  22696  chtppilimlem1  22721  rplogsumlem1  22732  dchrvmasumlem1  22743  dchrvmasum2lem  22744  chpdifbndlem1  22801  pntlemf  22853  brbtwn2  23150  colinearalglem4  23154  circum  27318  binomrisefac  27544  itgmulc2nc  28458  pellexlem6  29173  pell1234qrmulcl  29194  rmxyadd  29260  wallispi2lem2  29865  cevathlem1  29901
  Copyright terms: Public domain W3C validator