Theorem rexlimddv 2557

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1481   E.wrex 2418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-i5r 1516

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422  df-rex 2423

This theorem is referenced by:  disjiun  3932  nnsucpred  4538  grprinvlem  5973  grpridd  5975  tfrlemisucaccv  6230  tfrexlem  6239  tfr1onlemsucaccv  6246  tfrcllemsucaccv  6259  fict  6770  fidceq  6771  dif1enen  6782  php5fin  6784  fisbth  6785  fin0  6787  fin0or  6788  diffisn  6795  infnfi  6797  fientri3  6811  unsnfi  6815  unsnfidcex  6816  unsnfidcel  6817  fiuni  6874  ctmlemr  7001  ctssdccl  7004  fodjum  7026  fodju0  7027  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  cc2lem  7098  prarloclemarch2  7251  addlocpr  7368  nqprl  7383  nqpru  7384  appdiv0nq  7396  prmuloc  7398  mullocpr  7403  ltprordil  7421  ltaddpr  7429  ltexprlemopl  7433  ltexprlemopu  7435  ltexprlemloc  7439  ltexprlemrl  7442  ltexprlemru  7444  addcanprleml  7446  addcanprlemu  7447  ltaprlem  7450  ltaprg  7451  prplnqu  7452  recexprlemloc  7463  recexprlem1ssl  7465  recexprlem1ssu  7466  aptiprleml  7471  aptiprlemu  7472  ltmprr  7474  archpr  7475  cauappcvgprlemopl  7478  cauappcvgprlemopu  7480  cauappcvgprlemloc  7484  cauappcvgprlem1  7491  cauappcvgprlem2  7492  archrecpr  7496  caucvgprlemopl  7501  caucvgprlemopu  7503  caucvgprlemloc  7507  caucvgprlem2  7512  caucvgprprlemml  7526  caucvgprprlemmu  7527  caucvgprprlemopl  7529  caucvgprprlemopu  7531  caucvgprprlemloc  7535  caucvgprprlemexbt  7538  caucvgprprlem2  7542  suplocexprlemrl  7549  suplocexprlemmu  7550  suplocexprlemru  7551  suplocexprlemdisj  7552  suplocexprlemloc  7553  suplocexprlemex  7554  suplocexprlemub  7555  suplocexprlemlub  7556  prsrriota  7620  caucvgsrlemgt1  7627  caucvgsrlemoffres  7632  suplocsrlem  7640  rereceu  7721  recriota  7722  axarch  7723  axcaucvglemres  7731  axpre-suploclemres  7733  readdcan  7926  cnegex  7964  addcan  7966  addcan2  7967  negeu  7977  ltadd2  8205  recexre  8364  rimul  8371  ltmul1  8378  mulap0  8439  mulcanapd  8446  suprzclex  9173  qbtwnre  10065  hashcl  10559  hashen  10562  fihashdom  10581  hashunlem  10582  hashun  10583  zfz1iso  10616  cvg1nlemres  10789  cvg1n  10790  recvguniq  10799  resqrexlemoverl  10825  resqrexlemex  10829  fimaxre2  11030  climge0  11126  climrecvg1n  11149  fsum3cvg3  11197  expcnvre  11304  mertenslemub  11335  efcllem  11402  oexpneg  11610  zsupcllemex  11675  zssinfcl  11677  bezoutlemnewy  11720  bezoutlemstep  11721  dfgcd3  11734  bezout  11735  ennnfonelemex  11963  ennnfonelemrnh  11965  ennnfonelemf1  11967  ennnfonelemrn  11968  ennnfonelemdm  11969  ennnfonelemnn0  11971  ctinfomlemom  11976  ctinf  11979  ctiunctlemfo  11988  restbasg  12376  cnpnei  12427  cnptopco  12430  xmettx  12718  metcnpi3  12725  mulcncf  12799  dedekindeulemuub  12803  dedekindeulemub  12804  dedekindeulemlu  12807  dedekindicclemuub  12812  dedekindicclemub  12813  dedekindicclemlu  12816  dedekindicc  12819  ivthinclemlopn  12822  ivthinclemuopn  12824  limcimolemlt  12841  limcimo  12842  limccnp2cntop  12854  reeff1oleme  12901  eflt  12904  qdencn  13397  trilpolemlt1  13409