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

Theorem mul4d 9813
Description: Rearrangement of 4 factors. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
muld.1
addcomd.2
addcand.3
mul4d.4
Assertion
Ref Expression
mul4d

Proof of Theorem mul4d
StepHypRef Expression
1 muld.1 . 2
2 addcomd.2 . 2
3 addcand.3 . 2
4 mul4d.4 . 2
5 mul4 9770 . 2
61, 2, 3, 4, 5syl22anc 1229 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  (class class class)co 6296   cc 9511   cmul 9518
This theorem is referenced by:  remullem  12961  absmul  13127  cosadd  13900  tanadd  13902  eulerthlem2  14312  mul4sqlem  14471  odadd2  16855  itgmulc2  22240  plymullem1  22611  chordthmlem4  23166  heron  23169  quartlem1  23188  dchrmulcl  23524  bposlem9  23567  lgsdir  23605  lgsdi  23607  lgsquad2lem1  23633  chtppilimlem1  23658  rplogsumlem1  23669  dchrvmasumlem1  23680  dchrvmasum2lem  23681  chpdifbndlem1  23738  pntlemf  23790  brbtwn2  24208  colinearalglem4  24212  circum  29040  binomrisefac  29164  itgmulc2nc  30083  pellexlem6  30770  pell1234qrmulcl  30791  rmxyadd  30857  wallispi2lem2  31854  dirkertrigeqlem3  31882  cevathlem1  32084
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-mulcl 9575  ax-mulcom 9577  ax-mulass 9579
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299
  Copyright terms: Public domain W3C validator