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

Theorem rexlimddv 2953
Description: Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
Hypotheses
Ref Expression
rexlimddv.1
rexlimddv.2
Assertion
Ref Expression
rexlimddv
Distinct variable groups:   ,   ,

Proof of Theorem rexlimddv
StepHypRef Expression
1 rexlimddv.1 . 2
2 rexlimddv.2 . . 3
32rexlimdvaa 2950 . 2
41, 3mpd 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:  grprinvlem  6513  grpridd  6515  oaabs2  7313  oemapvali  8124  cantnflem4  8132  cantnflem4OLD  8154  r1pwss  8223  infxpenc2lem1  8417  pwfseqlem3  9059  prlem934  9432  ltexprlem7  9441  reclem3pr  9448  00id  9776  mul02lem1  9777  addid2  9784  addcan  9785  addcan2  9786  negeu  9833  mulcand  10207  suprzcl  10967  uzwo3  11206  expmulnbnd  12298  limsupgre  13304  rlimclim1  13368  fsumcvg3  13551  oexpneg  14049  bitsfi  14087  vdwlem10  14508  mreexexlem4d  15044  mreexdomd  15046  isacs3lem  15796  grprcan  16083  sylow1  16623  pgpfi  16625  slwhash  16644  pj1id  16717  efgsfo  16757  efgredlemc  16763  dmdprdsplitlem  17084  dmdprdsplitlemOLD  17085  dpjidcl  17107  dpjidclOLD  17114  pgpfac1lem4  17129  pgpfaclem2  17133  pgpfaclem3  17134  gsummgp0  17256  lspsolv  17789  restbas  19659  restcls  19682  restntr  19683  cnpnei  19765  cnpco  19768  pnrmopn  19844  1stcfb  19946  1stcrest  19954  2ndcctbss  19956  2ndcomap  19959  dis2ndc  19961  llyidm  19989  nllyidm  19990  hausllycmp  19995  lly1stc  19997  llycmpkgen2  20051  1stckgenlem  20054  basqtop  20212  regr1lem  20240  kqreglem1  20242  kqreglem2  20243  kqnrmlem1  20244  kqnrmlem2  20245  reghmph  20294  nrmhmph  20295  qtophmeo  20318  trfbas2  20344  fbasfip  20369  fbasrn  20385  trfg  20392  ssufl  20419  fmufil  20460  ufldom  20463  uffclsflim  20532  cnpfcfi  20541  alexsublem  20544  alexsubALTlem4  20550  ptcmplem3  20554  ptcmplem4  20555  tsmsxp  20657  met1stc  21024  met2ndci  21025  prdsxmslem2  21032  metcnpi3  21049  icccmplem1  21327  xrge0tsms  21339  metdseq0  21358  cnllycmp  21456  bndth  21458  lebnumlem1  21461  lebnum  21464  cfilfcls  21713  lmle  21740  relcmpcmet  21755  pjthlem2  21853  ovolscalem2  21925  ovolicc2lem4  21931  ovolicc2lem5  21932  ioombl1  21972  uniioombllem6  21997  uniioombl  21998  opnmbllem  22010  volivth  22016  mbfinf  22072  mbfi1fseqlem6  22127  itg2cnlem1  22168  itg2cn  22170  lhop2  22416  dvcnvre  22420  aareccl  22722  aaliou3lem8  22741  aaliou3lem9  22746  ulmdvlem3  22797  mtestbdd  22800  iblulm  22802  radcnvlem1  22808  abelthlem5  22830  abelthlem8  22834  chordthm  23168  dcubic  23177  fta  23353  dchrptlem2  23540  sumdchr2  23545  2sqlem11  23650  dchrisum  23677  dchrisum0flb  23695  pntibndlem3  23777  pntlemi  23789  pjspansn  26495  chscllem3  26557  xmulcand  27617  xrge0tsmsd  27775  esumpcvgval  28084  lgambdd  28579  lgamucov  28580  lgamcvglem  28582  lgamcvg2  28597  cnpcon  28675  pconcon  28676  conpcon  28680  pconpi1  28682  cnllyscon  28690  cvmcov2  28720  cvmliftpht  28763  mthmpps  28942  sinccvg  29039  btwnconn1lem13  29749  opnmbllem0  30050  mblfinlem2  30052  mblfinlem4  30054  neibastop2lem  30178  tailfb  30195  prdsbnd2  30291  cntotbnd  30292  heiborlem8  30314  heiborlem9  30315  acongrep  30918  jm2.27b  30948  lmhmfgsplit  31032  hbt  31079  cncmpmax  31407  stoweidlem62  31844  aacllem  33216  cvlcvr1  35064  llnmlplnN  35263  cdlemb  35518  paddasslem10  35553  trlcnv  35890  trlator0  35896  trlid0  35901  trlnidatb  35902  cdlemd4  35926  cdlemg5  36331  trlco  36453  cdlemj3  36549  tendo0mul  36552  tendo0mulr  36553  tendoconid  36555  erngdv  36719  erngdv-rN  36727  dihmeetlem1N  37017  dihatlat  37061  hgmaprnlem5N  37630  imo72b2lem1  37988
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