Theorem rexlimddv 2630

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 2626	. 2 |- ( ph -> ( E. x e. A ps -> ch ) )
4	1, 3	mpd 13	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2178   E.wrex 2487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2491  df-rex 2492

This theorem is referenced by:  disjiun  4054  nnsucpred  4683  tfrlemisucaccv  6434  tfrexlem  6443  tfr1onlemsucaccv  6450  tfrcllemsucaccv  6463  fict  6991  fidceq  6992  dif1enen  7003  php5fin  7005  fisbth  7006  fin0  7008  fin0or  7009  diffisn  7016  infnfi  7018  fientri3  7038  unsnfi  7042  unsnfidcex  7043  unsnfidcel  7044  fiuni  7106  ctmlemr  7236  ctssdccl  7239  fodjum  7274  fodju0  7275  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  cc2lem  7413  prarloclemarch2  7567  addlocpr  7684  nqprl  7699  nqpru  7700  appdiv0nq  7712  prmuloc  7714  mullocpr  7719  ltprordil  7737  ltaddpr  7745  ltexprlemopl  7749  ltexprlemopu  7751  ltexprlemloc  7755  ltexprlemrl  7758  ltexprlemru  7760  addcanprleml  7762  addcanprlemu  7763  ltaprlem  7766  ltaprg  7767  prplnqu  7768  recexprlemloc  7779  recexprlem1ssl  7781  recexprlem1ssu  7782  aptiprleml  7787  aptiprlemu  7788  ltmprr  7790  archpr  7791  cauappcvgprlemopl  7794  cauappcvgprlemopu  7796  cauappcvgprlemloc  7800  cauappcvgprlem1  7807  cauappcvgprlem2  7808  archrecpr  7812  caucvgprlemopl  7817  caucvgprlemopu  7819  caucvgprlemloc  7823  caucvgprlem2  7828  caucvgprprlemml  7842  caucvgprprlemmu  7843  caucvgprprlemopl  7845  caucvgprprlemopu  7847  caucvgprprlemloc  7851  caucvgprprlemexbt  7854  caucvgprprlem2  7858  suplocexprlemrl  7865  suplocexprlemmu  7866  suplocexprlemru  7867  suplocexprlemdisj  7868  suplocexprlemloc  7869  suplocexprlemex  7870  suplocexprlemub  7871  suplocexprlemlub  7872  prsrriota  7936  caucvgsrlemgt1  7943  caucvgsrlemoffres  7948  suplocsrlem  7956  rereceu  8037  recriota  8038  axarch  8039  axcaucvglemres  8047  axpre-suploclemres  8049  readdcan  8247  cnegex  8285  addcan  8287  addcan2  8288  negeu  8298  ltadd2  8527  recexre  8686  rimul  8693  ltmul1  8700  mulap0  8762  mulcanapd  8769  suprzclex  9506  zsupcllemex  10410  zssinfcl  10412  suprzubdc  10416  zsupssdc  10418  suprzcl2dc  10419  qbtwnre  10436  hashcl  10963  hashen  10966  fihashdom  10985  hashunlem  10986  hashun  10987  zfz1iso  11023  lencl  11035  sswrd  11040  cvg1nlemres  11411  cvg1n  11412  recvguniq  11421  resqrexlemoverl  11447  resqrexlemex  11451  fimaxre2  11653  climge0  11751  climrecvg1n  11774  fsum3cvg3  11822  expcnvre  11929  mertenslemub  11960  efcllem  12085  oexpneg  12303  bitsfzolem  12380  bitsfi  12383  bezoutlemnewy  12432  bezoutlemstep  12433  dfgcd3  12446  bezout  12447  isprm5lem  12578  ennnfonelemex  12900  ennnfonelemrnh  12902  ennnfonelemf1  12904  ennnfonelemrn  12905  ennnfonelemdm  12906  ennnfonelemnn0  12908  ctinfomlemom  12913  ctinf  12916  ctiunctlemfo  12925  nninfdclemcl  12934  nninfdc  12939  grpinvalem  13332  grprida  13334  grprcan  13484  mplsubgfilemcl  14576  restbasg  14755  cnpnei  14806  cnptopco  14809  xmettx  15097  metcnpi3  15104  mulcncf  15195  dedekindeulemuub  15204  dedekindeulemub  15205  dedekindeulemlu  15208  dedekindicclemuub  15213  dedekindicclemub  15214  dedekindicclemlu  15217  dedekindicc  15220  ivthinclemlopn  15223  ivthinclemuopn  15225  ivthreinc  15232  ivthdichlem  15238  limcimolemlt  15251  limcimo  15252  limccnp2cntop  15264  reeff1oleme  15359  eflt  15362  upgredg  15848  bj-charfunr  15945  qdencn  16168  trilpolemlt1  16182  nconstwlpolemgt0  16205