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

Theorem mul4d 9666
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 9623 . 2
61, 2, 3, 4, 5syl22anc 1220 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1370  e.wcel 1757  (class class class)co 6174   cc 9365   cmul 9372
This theorem is referenced by:  remullem  12703  absmul  12869  cosadd  13535  tanadd  13537  eulerthlem2  13943  mul4sqlem  14100  odadd2  16419  itgmulc2  21411  plymullem1  21782  chordthmlem4  22330  heron  22333  quartlem1  22352  dchrmulcl  22688  bposlem9  22731  lgsdir  22769  lgsdi  22771  lgsquad2lem1  22797  chtppilimlem1  22822  rplogsumlem1  22833  dchrvmasumlem1  22844  dchrvmasum2lem  22845  chpdifbndlem1  22902  pntlemf  22954  brbtwn2  23270  colinearalglem4  23274  circum  27437  binomrisefac  27663  itgmulc2nc  28582  pellexlem6  29297  pell1234qrmulcl  29318  rmxyadd  29384  wallispi2lem2  29989  cevathlem1  30025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-mulcl 9429  ax-mulcom 9431  ax-mulass 9433
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-rex 2798  df-rab 2801  df-v 3054  df-dif 3413  df-un 3415  df-in 3417  df-ss 3424  df-nul 3720  df-if 3874  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4174  df-br 4375  df-iota 5463  df-fv 5508  df-ov 6177
  Copyright terms: Public domain W3C validator