Theorem rexlimddv 2667

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

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

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 2527  df-rex 2528

This theorem is referenced by:  disjiun  4106  nnsucpred  4741  tfrlemisucaccv  6558  tfrexlem  6567  tfr1onlemsucaccv  6574  tfrcllemsucaccv  6587  fict  7125  fidceq  7126  dif1enen  7139  php5fin  7141  fisbth  7142  fin0  7144  fin0or  7145  diffisn  7152  infnfi  7154  fidcen  7158  fientri3  7177  unsnfi  7181  unsnfidcex  7182  unsnfidcel  7183  fiuni  7267  ctmlemr  7401  ctssdccl  7404  fodjum  7439  fodju0  7440  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  cc2lem  7582  prarloclemarch2  7736  addlocpr  7853  nqprl  7868  nqpru  7869  appdiv0nq  7881  prmuloc  7883  mullocpr  7888  ltprordil  7906  ltaddpr  7914  ltexprlemopl  7918  ltexprlemopu  7920  ltexprlemloc  7924  ltexprlemrl  7927  ltexprlemru  7929  addcanprleml  7931  addcanprlemu  7932  ltaprlem  7935  ltaprg  7936  prplnqu  7937  recexprlemloc  7948  recexprlem1ssl  7950  recexprlem1ssu  7951  aptiprleml  7956  aptiprlemu  7957  ltmprr  7959  archpr  7960  cauappcvgprlemopl  7963  cauappcvgprlemopu  7965  cauappcvgprlemloc  7969  cauappcvgprlem1  7976  cauappcvgprlem2  7977  archrecpr  7981  caucvgprlemopl  7986  caucvgprlemopu  7988  caucvgprlemloc  7992  caucvgprlem2  7997  caucvgprprlemml  8011  caucvgprprlemmu  8012  caucvgprprlemopl  8014  caucvgprprlemopu  8016  caucvgprprlemloc  8020  caucvgprprlemexbt  8023  caucvgprprlem2  8027  suplocexprlemrl  8034  suplocexprlemmu  8035  suplocexprlemru  8036  suplocexprlemdisj  8037  suplocexprlemloc  8038  suplocexprlemex  8039  suplocexprlemub  8040  suplocexprlemlub  8041  prsrriota  8105  caucvgsrlemgt1  8112  caucvgsrlemoffres  8117  suplocsrlem  8125  rereceu  8206  recriota  8207  axarch  8208  axcaucvglemres  8216  axpre-suploclemres  8218  readdcan  8415  cnegex  8453  addcan  8455  addcan2  8456  negeu  8466  ltadd2  8695  recexre  8854  rimul  8861  ltmul1  8868  mulap0  8930  mulcanapd  8937  suprzclex  9679  zsupcllemex  10594  zssinfcl  10596  suprzubdc  10600  zsupssdc  10602  suprzcl2dc  10603  qbtwnre  10620  hashcl  11148  hashen  11151  fihashdom  11171  hashunlem  11172  hashun  11173  zfz1iso  11217  lencl  11232  sswrd  11237  cvg1nlemres  11674  cvg1n  11675  recvguniq  11684  resqrexlemoverl  11710  resqrexlemex  11714  fimaxre2  11916  climge0  12014  climrecvg1n  12037  fsum3cvg3  12086  expcnvre  12193  mertenslemub  12224  efcllem  12349  oexpneg  12567  bitsfzolem  12644  bitsfi  12647  bezoutlemnewy  12696  bezoutlemstep  12697  dfgcd3  12710  bezout  12711  isprm5lem  12842  ennnfonelemex  13182  ennnfonelemrnh  13184  ennnfonelemf1  13186  ennnfonelemrn  13187  ennnfonelemdm  13188  ennnfonelemnn0  13190  ctinfomlemom  13195  ctinf  13198  ctiunctlemfo  13207  nninfdclemcl  13216  nninfdc  13221  grpinvalem  13615  grprida  13617  grprcan  13767  mplsubgfilemcl  14871  restbasg  15050  cnpnei  15101  cnptopco  15104  xmettx  15392  metcnpi3  15399  mulcncf  15490  dedekindeulemuub  15499  dedekindeulemub  15500  dedekindeulemlu  15503  dedekindicclemuub  15508  dedekindicclemub  15509  dedekindicclemlu  15512  dedekindicc  15515  ivthinclemlopn  15518  ivthinclemuopn  15520  ivthreinc  15527  ivthdichlem  15533  limcimolemlt  15546  limcimo  15547  limccnp2cntop  15559  reeff1oleme  15654  eflt  15657  upgredg  16156  bj-charfunr  16597  qdencn  16824  trilpolemlt1  16842  nconstwlpolemgt0  16867