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

Theorem reximddv 2933
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 7-Dec-2016.)
Hypotheses
Ref Expression
reximddva.1
reximddva.2
Assertion
Ref Expression
reximddv
Distinct variable group:   ,

Proof of Theorem reximddv
StepHypRef Expression
1 reximddva.2 . 2
2 reximddva.1 . . . 4
32expr 615 . . 3
43reximdva 2932 . 2
51, 4mpd 15 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  E.wrex 2808
This theorem is referenced by:  reximddv2  2934  dedekind  9765  caucvgrlem  13495  isprm5  14253  drsdirfi  15567  sylow2  16646  gexex  16859  nrmsep  19858  regsep2  19877  locfincmp  20027  dissnref  20029  met1stc  21024  xrge0tsms  21339  cnheibor  21455  lmcau  21751  ismbf3d  22061  ulmdvlem3  22797  legov  23972  legtrid  23978  midexlem  24069  opphllem  24109  mideulem  24110  midex  24111  hpgid  24135  grpoidinv  25210  pjhthlem2  26310  mdsymlem3  27324  xrge0tsmsd  27775  ballotlemfc0  28431  ballotlemfcc  28432  cvmliftlem15  28743  nacsfix  30644  unxpwdom3  31041  rfcnnnub  31411  stoweidlem27  31809  lhpexle3lem  35735  lhpex2leN  35737  cdlemg1cex  36314
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
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-ral 2812  df-rex 2813
  Copyright terms: Public domain W3C validator