Theorem rexlimddv 2656

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516  df-rex 2517

This theorem is referenced by:  disjiun  4088  nnsucpred  4721  tfrlemisucaccv  6534  tfrexlem  6543  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  fict  7098  fidceq  7099  dif1enen  7112  php5fin  7114  fisbth  7115  fin0  7117  fin0or  7118  diffisn  7125  infnfi  7127  fidcen  7131  fientri3  7150  unsnfi  7154  unsnfidcex  7155  unsnfidcel  7156  fiuni  7237  ctmlemr  7367  ctssdccl  7370  fodjum  7405  fodju0  7406  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  cc2lem  7545  prarloclemarch2  7699  addlocpr  7816  nqprl  7831  nqpru  7832  appdiv0nq  7844  prmuloc  7846  mullocpr  7851  ltprordil  7869  ltaddpr  7877  ltexprlemopl  7881  ltexprlemopu  7883  ltexprlemloc  7887  ltexprlemrl  7890  ltexprlemru  7892  addcanprleml  7894  addcanprlemu  7895  ltaprlem  7898  ltaprg  7899  prplnqu  7900  recexprlemloc  7911  recexprlem1ssl  7913  recexprlem1ssu  7914  aptiprleml  7919  aptiprlemu  7920  ltmprr  7922  archpr  7923  cauappcvgprlemopl  7926  cauappcvgprlemopu  7928  cauappcvgprlemloc  7932  cauappcvgprlem1  7939  cauappcvgprlem2  7940  archrecpr  7944  caucvgprlemopl  7949  caucvgprlemopu  7951  caucvgprlemloc  7955  caucvgprlem2  7960  caucvgprprlemml  7974  caucvgprprlemmu  7975  caucvgprprlemopl  7977  caucvgprprlemopu  7979  caucvgprprlemloc  7983  caucvgprprlemexbt  7986  caucvgprprlem2  7990  suplocexprlemrl  7997  suplocexprlemmu  7998  suplocexprlemru  7999  suplocexprlemdisj  8000  suplocexprlemloc  8001  suplocexprlemex  8002  suplocexprlemub  8003  suplocexprlemlub  8004  prsrriota  8068  caucvgsrlemgt1  8075  caucvgsrlemoffres  8080  suplocsrlem  8088  rereceu  8169  recriota  8170  axarch  8171  axcaucvglemres  8179  axpre-suploclemres  8181  readdcan  8378  cnegex  8416  addcan  8418  addcan2  8419  negeu  8429  ltadd2  8658  recexre  8817  rimul  8824  ltmul1  8831  mulap0  8893  mulcanapd  8900  suprzclex  9639  zsupcllemex  10553  zssinfcl  10555  suprzubdc  10559  zsupssdc  10561  suprzcl2dc  10562  qbtwnre  10579  hashcl  11106  hashen  11109  fihashdom  11129  hashunlem  11130  hashun  11131  zfz1iso  11168  lencl  11183  sswrd  11188  cvg1nlemres  11625  cvg1n  11626  recvguniq  11635  resqrexlemoverl  11661  resqrexlemex  11665  fimaxre2  11867  climge0  11965  climrecvg1n  11988  fsum3cvg3  12037  expcnvre  12144  mertenslemub  12175  efcllem  12300  oexpneg  12518  bitsfzolem  12595  bitsfi  12598  bezoutlemnewy  12647  bezoutlemstep  12648  dfgcd3  12661  bezout  12662  isprm5lem  12793  ennnfonelemex  13115  ennnfonelemrnh  13117  ennnfonelemf1  13119  ennnfonelemrn  13120  ennnfonelemdm  13121  ennnfonelemnn0  13123  ctinfomlemom  13128  ctinf  13131  ctiunctlemfo  13140  nninfdclemcl  13149  nninfdc  13154  grpinvalem  13548  grprida  13550  grprcan  13700  mplsubgfilemcl  14800  restbasg  14979  cnpnei  15030  cnptopco  15033  xmettx  15321  metcnpi3  15328  mulcncf  15419  dedekindeulemuub  15428  dedekindeulemub  15429  dedekindeulemlu  15432  dedekindicclemuub  15437  dedekindicclemub  15438  dedekindicclemlu  15441  dedekindicc  15444  ivthinclemlopn  15447  ivthinclemuopn  15449  ivthreinc  15456  ivthdichlem  15462  limcimolemlt  15475  limcimo  15476  limccnp2cntop  15488  reeff1oleme  15583  eflt  15586  upgredg  16085  bj-charfunr  16526  qdencn  16755  trilpolemlt1  16773  nconstwlpolemgt0  16797