Theorem rexlimddv 2628

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

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-i5r 1558

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489  df-rex 2490

This theorem is referenced by:  disjiun  4039  nnsucpred  4665  tfrlemisucaccv  6411  tfrexlem  6420  tfr1onlemsucaccv  6427  tfrcllemsucaccv  6440  fict  6965  fidceq  6966  dif1enen  6977  php5fin  6979  fisbth  6980  fin0  6982  fin0or  6983  diffisn  6990  infnfi  6992  fientri3  7012  unsnfi  7016  unsnfidcex  7017  unsnfidcel  7018  fiuni  7080  ctmlemr  7210  ctssdccl  7213  fodjum  7248  fodju0  7249  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  cc2lem  7378  prarloclemarch2  7532  addlocpr  7649  nqprl  7664  nqpru  7665  appdiv0nq  7677  prmuloc  7679  mullocpr  7684  ltprordil  7702  ltaddpr  7710  ltexprlemopl  7714  ltexprlemopu  7716  ltexprlemloc  7720  ltexprlemrl  7723  ltexprlemru  7725  addcanprleml  7727  addcanprlemu  7728  ltaprlem  7731  ltaprg  7732  prplnqu  7733  recexprlemloc  7744  recexprlem1ssl  7746  recexprlem1ssu  7747  aptiprleml  7752  aptiprlemu  7753  ltmprr  7755  archpr  7756  cauappcvgprlemopl  7759  cauappcvgprlemopu  7761  cauappcvgprlemloc  7765  cauappcvgprlem1  7772  cauappcvgprlem2  7773  archrecpr  7777  caucvgprlemopl  7782  caucvgprlemopu  7784  caucvgprlemloc  7788  caucvgprlem2  7793  caucvgprprlemml  7807  caucvgprprlemmu  7808  caucvgprprlemopl  7810  caucvgprprlemopu  7812  caucvgprprlemloc  7816  caucvgprprlemexbt  7819  caucvgprprlem2  7823  suplocexprlemrl  7830  suplocexprlemmu  7831  suplocexprlemru  7832  suplocexprlemdisj  7833  suplocexprlemloc  7834  suplocexprlemex  7835  suplocexprlemub  7836  suplocexprlemlub  7837  prsrriota  7901  caucvgsrlemgt1  7908  caucvgsrlemoffres  7913  suplocsrlem  7921  rereceu  8002  recriota  8003  axarch  8004  axcaucvglemres  8012  axpre-suploclemres  8014  readdcan  8212  cnegex  8250  addcan  8252  addcan2  8253  negeu  8263  ltadd2  8492  recexre  8651  rimul  8658  ltmul1  8665  mulap0  8727  mulcanapd  8734  suprzclex  9471  zsupcllemex  10373  zssinfcl  10375  suprzubdc  10379  zsupssdc  10381  suprzcl2dc  10382  qbtwnre  10399  hashcl  10926  hashen  10929  fihashdom  10948  hashunlem  10949  hashun  10950  zfz1iso  10986  lencl  10998  sswrd  11003  cvg1nlemres  11296  cvg1n  11297  recvguniq  11306  resqrexlemoverl  11332  resqrexlemex  11336  fimaxre2  11538  climge0  11636  climrecvg1n  11659  fsum3cvg3  11707  expcnvre  11814  mertenslemub  11845  efcllem  11970  oexpneg  12188  bitsfzolem  12265  bitsfi  12268  bezoutlemnewy  12317  bezoutlemstep  12318  dfgcd3  12331  bezout  12332  isprm5lem  12463  ennnfonelemex  12785  ennnfonelemrnh  12787  ennnfonelemf1  12789  ennnfonelemrn  12790  ennnfonelemdm  12791  ennnfonelemnn0  12793  ctinfomlemom  12798  ctinf  12801  ctiunctlemfo  12810  nninfdclemcl  12819  nninfdc  12824  grpinvalem  13217  grprida  13219  grprcan  13369  mplsubgfilemcl  14461  restbasg  14640  cnpnei  14691  cnptopco  14694  xmettx  14982  metcnpi3  14989  mulcncf  15080  dedekindeulemuub  15089  dedekindeulemub  15090  dedekindeulemlu  15093  dedekindicclemuub  15098  dedekindicclemub  15099  dedekindicclemlu  15102  dedekindicc  15105  ivthinclemlopn  15108  ivthinclemuopn  15110  ivthreinc  15117  ivthdichlem  15123  limcimolemlt  15136  limcimo  15137  limccnp2cntop  15149  reeff1oleme  15244  eflt  15247  bj-charfunr  15746  qdencn  15966  trilpolemlt1  15980  nconstwlpolemgt0  16003