Theorem rexlimddv 2599

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

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

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  disjiun  4000  nnsucpred  4618  tfrlemisucaccv  6328  tfrexlem  6337  tfr1onlemsucaccv  6344  tfrcllemsucaccv  6357  fict  6870  fidceq  6871  dif1enen  6882  php5fin  6884  fisbth  6885  fin0  6887  fin0or  6888  diffisn  6895  infnfi  6897  fientri3  6916  unsnfi  6920  unsnfidcex  6921  unsnfidcel  6922  fiuni  6979  ctmlemr  7109  ctssdccl  7112  fodjum  7146  fodju0  7147  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  cc2lem  7267  prarloclemarch2  7420  addlocpr  7537  nqprl  7552  nqpru  7553  appdiv0nq  7565  prmuloc  7567  mullocpr  7572  ltprordil  7590  ltaddpr  7598  ltexprlemopl  7602  ltexprlemopu  7604  ltexprlemloc  7608  ltexprlemrl  7611  ltexprlemru  7613  addcanprleml  7615  addcanprlemu  7616  ltaprlem  7619  ltaprg  7620  prplnqu  7621  recexprlemloc  7632  recexprlem1ssl  7634  recexprlem1ssu  7635  aptiprleml  7640  aptiprlemu  7641  ltmprr  7643  archpr  7644  cauappcvgprlemopl  7647  cauappcvgprlemopu  7649  cauappcvgprlemloc  7653  cauappcvgprlem1  7660  cauappcvgprlem2  7661  archrecpr  7665  caucvgprlemopl  7670  caucvgprlemopu  7672  caucvgprlemloc  7676  caucvgprlem2  7681  caucvgprprlemml  7695  caucvgprprlemmu  7696  caucvgprprlemopl  7698  caucvgprprlemopu  7700  caucvgprprlemloc  7704  caucvgprprlemexbt  7707  caucvgprprlem2  7711  suplocexprlemrl  7718  suplocexprlemmu  7719  suplocexprlemru  7720  suplocexprlemdisj  7721  suplocexprlemloc  7722  suplocexprlemex  7723  suplocexprlemub  7724  suplocexprlemlub  7725  prsrriota  7789  caucvgsrlemgt1  7796  caucvgsrlemoffres  7801  suplocsrlem  7809  rereceu  7890  recriota  7891  axarch  7892  axcaucvglemres  7900  axpre-suploclemres  7902  readdcan  8099  cnegex  8137  addcan  8139  addcan2  8140  negeu  8150  ltadd2  8378  recexre  8537  rimul  8544  ltmul1  8551  mulap0  8613  mulcanapd  8620  suprzclex  9353  qbtwnre  10259  hashcl  10763  hashen  10766  fihashdom  10785  hashunlem  10786  hashun  10787  zfz1iso  10823  cvg1nlemres  10996  cvg1n  10997  recvguniq  11006  resqrexlemoverl  11032  resqrexlemex  11036  fimaxre2  11237  climge0  11335  climrecvg1n  11358  fsum3cvg3  11406  expcnvre  11513  mertenslemub  11544  efcllem  11669  oexpneg  11884  zsupcllemex  11949  zssinfcl  11951  suprzubdc  11955  zsupssdc  11957  suprzcl2dc  11958  bezoutlemnewy  11999  bezoutlemstep  12000  dfgcd3  12013  bezout  12014  isprm5lem  12143  ennnfonelemex  12417  ennnfonelemrnh  12419  ennnfonelemf1  12421  ennnfonelemrn  12422  ennnfonelemdm  12423  ennnfonelemnn0  12425  ctinfomlemom  12430  ctinf  12433  ctiunctlemfo  12442  nninfdclemcl  12451  nninfdc  12456  grprinvlem  12809  grpridd  12811  grprcan  12915  restbasg  13753  cnpnei  13804  cnptopco  13807  xmettx  14095  metcnpi3  14102  mulcncf  14176  dedekindeulemuub  14180  dedekindeulemub  14181  dedekindeulemlu  14184  dedekindicclemuub  14189  dedekindicclemub  14190  dedekindicclemlu  14193  dedekindicc  14196  ivthinclemlopn  14199  ivthinclemuopn  14201  limcimolemlt  14218  limcimo  14219  limccnp2cntop  14231  reeff1oleme  14278  eflt  14281  bj-charfunr  14647  qdencn  14860  trilpolemlt1  14874  nconstwlpolemgt0  14897