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

Theorem reximdva 2932
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)
Hypothesis
Ref Expression
reximdva.1
Assertion
Ref Expression
reximdva
Distinct variable group:   ,

Proof of Theorem reximdva
StepHypRef Expression
1 reximdva.1 . . 3
21ex 434 . 2
32reximdvai 2929 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  E.wrex 2808
This theorem is referenced by:  reximddv  2933  reximddv2  2934  wereu2  4881  dffo4  6047  nnaordex  7306  frfi  7785  fisupg  7788  marypha1  7914  wemapsolem  7996  unwdomg  8031  noinfepOLD  8098  rankr1ai  8237  cofsmo  8670  cfcoflem  8673  inar1  9174  nqerf  9329  prlem936  9446  fimaxre  10515  arch  10817  bndndx  10819  suprfinzcl  11003  zmin  11207  qbtwnxr  11428  qsqueeze  11429  qextltlem  11430  xrsupsslem  11527  xrinfmsslem  11528  xrub  11532  supxrunb1  11540  ssnn0fi  12094  fsuppmapnn0fiub0  12099  fsuppmapnn0fz  12102  expnlbnd2  12297  r19.29uz  13183  cau3lem  13187  rlim2lt  13320  rlimclim  13369  2clim  13395  o1co  13409  climcn1  13414  climcn2  13415  rlimo1  13439  climsqz  13463  climsqz2  13464  rlimsqzlem  13471  lo1le  13474  climsup  13492  climcau  13493  caucvgrlem2  13497  iseralt  13507  cvgcmp  13630  cvgcmpce  13632  supcvg  13667  rpnnen2  13959  bezoutlem1  14176  exprmfct  14251  pclem  14362  pc2dvds  14402  pcprmpw  14406  unbenlem  14426  infpnlem2  14429  infpn2  14431  prmunb  14432  vdwlem2  14500  ramub1lem2  14545  ipodrsima  15795  grpinveu  16084  psgneu  16531  odbezout  16580  sylow2blem3  16642  nn0gsumfz  17012  irredrmul  17356  lsmelval2  17731  lbsextlem2  17805  mptcoe1fsupp  18255  znunit  18602  scmate  19012  scmatscm  19015  scmatfo  19032  mat1scmat  19041  pmatcoe1fsupp  19202  pmatcollpwfi  19283  pmatcollpw3fi  19286  mptcoe1matfsupp  19303  pm2mp  19326  chmaidscmat  19349  cpmadugsum  19379  cpmadumatpoly  19384  chcoeffeq  19387  cayhamlem3  19388  cayhamlem4  19389  neiptopnei  19633  neitr  19681  cnpnei  19765  haust1  19853  isnrm3  19860  isreg2  19878  tgcmp  19901  hauscmplem  19906  hauscmp  19907  bwth  19910  1stcfb  19946  1stcelcls  19962  lly1stc  19997  txcmplem1  20142  txlm  20149  xkococnlem  20160  filuni  20386  filufint  20421  ufilen  20431  fclscf  20526  cnextcn  20567  ustex2sym  20719  ustex3sym  20720  utopreg  20755  isucn2  20782  ucnima  20784  ucncn  20788  neipcfilu  20799  metequiv2  21013  metrest  21027  xrsmopn  21317  mulc1cncf  21409  cncfco  21411  bndth  21458  lmmcvg  21700  cfil3i  21708  iscau4  21718  cmetcaulem  21727  iscmet3lem1  21730  caussi  21736  equivcfil  21738  equivcau  21739  caubl  21746  minveclem3b  21843  ovolgelb  21891  ovollb2lem  21899  ovolctb  21901  ovolicc2lem4  21931  ioombl1lem4  21971  dyadmax  22007  volsup2  22014  itg2monolem1  22157  c1liplem1  22397  c1lip1  22398  dvivthlem1  22409  lhop1  22415  ftc1a  22438  ftc1lem6  22442  ply1divex  22537  elply2  22593  dgrlem  22626  aacjcl  22723  aalioulem2  22729  aalioulem3  22730  aalioulem4  22731  ulmcaulem  22789  ulmcau  22790  ulmss  22792  mtest  22799  itgulm  22803  reeff1o  22842  efif1olem4  22932  rlimcnp  23295  xrlimcnp  23298  ftalem3  23348  fta  23353  muval1  23407  dvdssqf  23412  mumullem1  23453  pntlem3  23794  ostth  23824  tgtrisegint  23890  tgbtwndiff  23897  tgcgrxfr  23909  lnext  23954  legov2  23973  legtrd  23976  colperpexlem3  24106  colperpex  24107  hpgerlem  24134  hpgtr  24137  axpasch  24244  wwlknredwwlkn0  24727  2pthfrgrarn2  25010  frgrawopreglem5  25048  usgreg2spot  25067  grpoidinvlem3  25208  grpoideu  25211  grpoinveu  25224  isgrp2d  25237  rngo2  25390  ubthlem1  25786  minvecolem5  25797  htthlem  25834  chscllem2  26556  nmopun  26933  lnconi  26952  rnbra  27026  sumdmdii  27334  cdj3lem2b  27356  foresf1o  27403  xrofsup  27582  isarchi3  27731  isarchiofld  27807  lmxrge0  27934  lmdvg  27935  esumlub  28068  esumfsup  28076  esumcvg  28092  eulerpartlemgvv  28315  lgamucov  28580  cvmliftmolem2  28727  cvmlift2lem10  28757  cvmlift2lem12  28759  frmin  29322  wzel  29380  wsuclem  29381  nofulllem5  29466  btwndiff  29677  trisegint  29678  cgrxfr  29705  lineext  29726  segcon2  29755  brsegle2  29759  seglecgr12im  29760  segletr  29764  broutsideof3  29776  fin2so  30040  mblfinlem1  30051  mblfinlem2  30052  mblfinlem3  30053  mblfinlem4  30054  itg2addnclem  30066  ftc1cnnc  30089  ftc1anclem5  30094  ftc1anclem6  30095  opnrebl2  30139  nn0prpw  30141  sdclem1  30236  geomcau  30252  equivtotbnd  30274  bndss  30282  ismtybndlem  30302  heibor1lem  30305  rrncmslem  30328  prtlem15  30616  fphpdo  30751  rencldnfilem  30754  irrapxlem2  30759  cvgdvgrat  31194  lcmgcdlem  31212  expgrowth  31240  ssfiunibd  31509  climinf  31612  mullimc  31622  islptre  31625  limccog  31626  mullimcf  31629  limcrecl  31635  sumnnodd  31636  neglimc  31653  0ellimcdiv  31655  limclner  31657  cncfioobd  31700  stoweidlem7  31789  stoweidlem27  31809  stoweidlem39  31821  stoweidlem48  31830  stoweidlem49  31831  stoweidlem60  31842  stoweidlem61  31843  stoweid  31845  dirkercncflem2  31886  fourierdlem20  31909  fourierdlem39  31928  fourierdlem41  31930  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem64  31953  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem87  31976  fourierdlem103  31992  fourierdlem104  31993  zrninitoringc  32879  ply1mulgsumlem3  32988  ply1mulgsumlem4  32989  islindeps2  33084  isldepslvec2  33086  lsateln0  34720  lsat0cv  34758  eqlkr3  34826  lkrshp  34830  lshpset2N  34844  hlhgt2  35113  hlrelat2  35127  atle  35160  athgt  35180  2dim  35194  1cvratex  35197  ps-2  35202  dalem20  35417  lhpexle1lem  35731  lhpexle1  35732  lhpexle2lem  35733  lhpmcvr5N  35751  lhpmcvr6N  35752  cdleme25a  36079  cdleme29ex  36100  cdlemfnid  36290  cdlemg33b0  36427  cdlemg33a  36432  cdlemg35  36439  cdleml3N  36704  dihlsscpre  36961  dih1dimb2  36968  dihatexv  37065  dvh3dim2  37175  dochkr1  37205  dochkr1OLDN  37206  lcfl8  37229  lcfl8b  37231  lcfrlem5  37273  lcfrlem6  37274  mapdrvallem2  37372  mapdh9a  37517  mapdh9aOLDN  37518  hdmaprnlem3eN  37588  hdmaprnlem16N  37592
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