Theorem rexlimddv 3035

Description: Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)

Hypotheses

Ref	Expression
rexlimddv.1	|- ( ph -> E. x e. A ps )
rexlimddv.2	|- ( ( ph /\ ( x e. A /\ ps ) ) -> ch )

Assertion

Ref	Expression
rexlimddv	|- ( ph -> ch )

Distinct variable groups:   ph, x   ch, x

Allowed substitution hints:   ps( x)   A( x)

Proof of Theorem rexlimddv

Step	Hyp	Ref	Expression
1		rexlimddv.1	. 2 |- ( ph -> E. x e. A ps )
2		rexlimddv.2	. . 3 |- ( ( ph /\ ( x e. A /\ ps ) ) -> ch )
3	2	rexlimdvaa 3032	. 2 |- ( ph -> ( E. x e. A ps -> ch ) )
4	1, 3	mpd 15	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  grprinvlem  6872  grpridd  6874  oaabs2  7725  oemapvali  8581  cantnflem4  8589  r1pwss  8647  infxpenc2lem1  8842  pwfseqlem3  9482  prlem934  9855  ltexprlem7  9864  reclem3pr  9871  00id  10211  mul02lem1  10212  addid2  10219  addcan  10220  addcan2  10221  negeu  10271  mulcand  10660  suprzcl  11457  uzwo3  11783  expmulnbnd  12996  limsupgre  14212  rlimclim1  14276  fsumcvg3  14460  oexpneg  15069  bitsfi  15159  vdwlem10  15694  mreexexlem4d  16307  mreexdomd  16310  isacs3lem  17166  grprcan  17455  sylow1  18018  pgpfi  18020  slwhash  18039  pj1id  18112  efgsfo  18152  efgredlemc  18158  dmdprdsplitlem  18436  dpjidcl  18457  pgpfac1lem4  18477  pgpfaclem2  18481  pgpfaclem3  18482  gsummgp0  18608  lspsolv  19143  restbas  20962  restcls  20985  restntr  20986  cnpnei  21068  cnpco  21071  pnrmopn  21147  1stcfb  21248  1stcrest  21256  2ndcctbss  21258  2ndcomap  21261  dis2ndc  21263  llyidm  21291  nllyidm  21292  hausllycmp  21297  lly1stc  21299  llycmpkgen2  21353  1stckgenlem  21356  basqtop  21514  regr1lem  21542  kqreglem1  21544  kqreglem2  21545  kqnrmlem1  21546  kqnrmlem2  21547  reghmph  21596  nrmhmph  21597  qtophmeo  21620  trfbas2  21647  fbasfip  21672  fbasrn  21688  trfg  21695  ssufl  21722  fmufil  21763  ufldom  21766  uffclsflim  21835  cnpfcfi  21844  alexsublem  21848  alexsubALTlem4  21854  ptcmplem3  21858  ptcmplem4  21859  tsmsxp  21958  met1stc  22326  met2ndci  22327  prdsxmslem2  22334  metcnpi3  22351  icccmplem1  22625  xrge0tsms  22637  metdseq0  22657  cnllycmp  22755  bndth  22757  lebnumlem1  22760  lebnum  22763  cfilfcls  23072  lmle  23099  relcmpcmet  23115  pjthlem2  23209  ovolscalem2  23282  ovolicc2lem4  23288  ovolicc2lem5  23289  ioombl1  23330  uniioombllem6  23356  uniioombl  23357  opnmbllem  23369  volivth  23375  mbfinf  23432  mbfi1fseqlem6  23487  itg2cnlem1  23528  itg2cn  23530  lhop2  23778  dvcnvre  23782  aareccl  24081  aaliou3lem8  24100  aaliou3lem9  24105  ulmdvlem3  24156  mtestbdd  24159  iblulm  24161  radcnvlem1  24167  abelthlem5  24189  abelthlem8  24193  chordthm  24564  dcubic  24573  lgambdd  24763  lgamucov  24764  lgamcvglem  24766  lgamcvg2  24781  fta  24806  dchrptlem2  24990  sumdchr2  24995  2sqlem11  25154  dchrisum  25181  dchrisum0flb  25199  pntibndlem3  25281  pntlemi  25293  pjspansn  28436  chscllem3  28498  xmulcand  29629  xrge0tsmsd  29785  esumpcvgval  30140  cnpconn  31212  pconnconn  31213  connpconn  31217  pconnpi1  31219  cnllysconn  31227  cvmcov2  31257  cvmliftpht  31300  mthmpps  31479  sinccvg  31567  btwnconn1lem13  32206  neibastop2lem  32355  tailfb  32372  unblimceq0lem  32497  knoppndvlem9  32511  knoppndvlem21  32523  knoppndvlem22  32524  matunitlindflem2  33406  poimirlem29  33438  opnmbllem0  33445  mblfinlem2  33447  mblfinlem4  33449  prdsbnd2  33594  cntotbnd  33595  heiborlem8  33617  heiborlem9  33618  cvlcvr1  34626  llnmlplnN  34825  cdlemb  35080  paddasslem10  35115  trlcnv  35452  trlator0  35458  trlid0  35463  trlnidatb  35464  cdlemd4  35488  cdlemg5  35893  trlco  36015  cdlemj3  36111  tendo0mul  36114  tendo0mulr  36115  tendoconid  36117  erngdv  36281  erngdv-rN  36289  dihmeetlem1N  36579  dihatlat  36623  hgmaprnlem5N  37192  acongrep  37547  jm2.27b  37573  lmhmfgsplit  37656  hbt  37700  imo72b2lem1  38471  cncmpmax  39191  rexlimddv2  40049  stoweidlem62  40279  oexpnegALTV  41588  oexpnegnz  41589  aacllem  42547