Theorem rexlimddv 2653

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

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  disjiun  4078  nnsucpred  4709  tfrlemisucaccv  6471  tfrexlem  6480  tfr1onlemsucaccv  6487  tfrcllemsucaccv  6500  fict  7030  fidceq  7031  dif1enen  7042  php5fin  7044  fisbth  7045  fin0  7047  fin0or  7048  diffisn  7055  infnfi  7057  fientri3  7077  unsnfi  7081  unsnfidcex  7082  unsnfidcel  7083  fiuni  7145  ctmlemr  7275  ctssdccl  7278  fodjum  7313  fodju0  7314  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  cc2lem  7452  prarloclemarch2  7606  addlocpr  7723  nqprl  7738  nqpru  7739  appdiv0nq  7751  prmuloc  7753  mullocpr  7758  ltprordil  7776  ltaddpr  7784  ltexprlemopl  7788  ltexprlemopu  7790  ltexprlemloc  7794  ltexprlemrl  7797  ltexprlemru  7799  addcanprleml  7801  addcanprlemu  7802  ltaprlem  7805  ltaprg  7806  prplnqu  7807  recexprlemloc  7818  recexprlem1ssl  7820  recexprlem1ssu  7821  aptiprleml  7826  aptiprlemu  7827  ltmprr  7829  archpr  7830  cauappcvgprlemopl  7833  cauappcvgprlemopu  7835  cauappcvgprlemloc  7839  cauappcvgprlem1  7846  cauappcvgprlem2  7847  archrecpr  7851  caucvgprlemopl  7856  caucvgprlemopu  7858  caucvgprlemloc  7862  caucvgprlem2  7867  caucvgprprlemml  7881  caucvgprprlemmu  7882  caucvgprprlemopl  7884  caucvgprprlemopu  7886  caucvgprprlemloc  7890  caucvgprprlemexbt  7893  caucvgprprlem2  7897  suplocexprlemrl  7904  suplocexprlemmu  7905  suplocexprlemru  7906  suplocexprlemdisj  7907  suplocexprlemloc  7908  suplocexprlemex  7909  suplocexprlemub  7910  suplocexprlemlub  7911  prsrriota  7975  caucvgsrlemgt1  7982  caucvgsrlemoffres  7987  suplocsrlem  7995  rereceu  8076  recriota  8077  axarch  8078  axcaucvglemres  8086  axpre-suploclemres  8088  readdcan  8286  cnegex  8324  addcan  8326  addcan2  8327  negeu  8337  ltadd2  8566  recexre  8725  rimul  8732  ltmul1  8739  mulap0  8801  mulcanapd  8808  suprzclex  9545  zsupcllemex  10450  zssinfcl  10452  suprzubdc  10456  zsupssdc  10458  suprzcl2dc  10459  qbtwnre  10476  hashcl  11003  hashen  11006  fihashdom  11025  hashunlem  11026  hashun  11027  zfz1iso  11063  lencl  11075  sswrd  11080  cvg1nlemres  11496  cvg1n  11497  recvguniq  11506  resqrexlemoverl  11532  resqrexlemex  11536  fimaxre2  11738  climge0  11836  climrecvg1n  11859  fsum3cvg3  11907  expcnvre  12014  mertenslemub  12045  efcllem  12170  oexpneg  12388  bitsfzolem  12465  bitsfi  12468  bezoutlemnewy  12517  bezoutlemstep  12518  dfgcd3  12531  bezout  12532  isprm5lem  12663  ennnfonelemex  12985  ennnfonelemrnh  12987  ennnfonelemf1  12989  ennnfonelemrn  12990  ennnfonelemdm  12991  ennnfonelemnn0  12993  ctinfomlemom  12998  ctinf  13001  ctiunctlemfo  13010  nninfdclemcl  13019  nninfdc  13024  grpinvalem  13418  grprida  13420  grprcan  13570  mplsubgfilemcl  14663  restbasg  14842  cnpnei  14893  cnptopco  14896  xmettx  15184  metcnpi3  15191  mulcncf  15282  dedekindeulemuub  15291  dedekindeulemub  15292  dedekindeulemlu  15295  dedekindicclemuub  15300  dedekindicclemub  15301  dedekindicclemlu  15304  dedekindicc  15307  ivthinclemlopn  15310  ivthinclemuopn  15312  ivthreinc  15319  ivthdichlem  15325  limcimolemlt  15338  limcimo  15339  limccnp2cntop  15351  reeff1oleme  15446  eflt  15449  upgredg  15942  bj-charfunr  16173  qdencn  16395  trilpolemlt1  16409  nconstwlpolemgt0  16432