Theorem rexlimddv 2554

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

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

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-i5r 1515

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421  df-rex 2422

This theorem is referenced by:  disjiun  3924  nnsucpred  4530  grprinvlem  5965  grpridd  5967  tfrlemisucaccv  6222  tfrexlem  6231  tfr1onlemsucaccv  6238  tfrcllemsucaccv  6251  fict  6762  fidceq  6763  dif1enen  6774  php5fin  6776  fisbth  6777  fin0  6779  fin0or  6780  diffisn  6787  infnfi  6789  fientri3  6803  unsnfi  6807  unsnfidcex  6808  unsnfidcel  6809  fiuni  6866  ctmlemr  6993  ctssdccl  6996  fodjum  7018  fodju0  7019  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  prarloclemarch2  7227  addlocpr  7344  nqprl  7359  nqpru  7360  appdiv0nq  7372  prmuloc  7374  mullocpr  7379  ltprordil  7397  ltaddpr  7405  ltexprlemopl  7409  ltexprlemopu  7411  ltexprlemloc  7415  ltexprlemrl  7418  ltexprlemru  7420  addcanprleml  7422  addcanprlemu  7423  ltaprlem  7426  ltaprg  7427  prplnqu  7428  recexprlemloc  7439  recexprlem1ssl  7441  recexprlem1ssu  7442  aptiprleml  7447  aptiprlemu  7448  ltmprr  7450  archpr  7451  cauappcvgprlemopl  7454  cauappcvgprlemopu  7456  cauappcvgprlemloc  7460  cauappcvgprlem1  7467  cauappcvgprlem2  7468  archrecpr  7472  caucvgprlemopl  7477  caucvgprlemopu  7479  caucvgprlemloc  7483  caucvgprlem2  7488  caucvgprprlemml  7502  caucvgprprlemmu  7503  caucvgprprlemopl  7505  caucvgprprlemopu  7507  caucvgprprlemloc  7511  caucvgprprlemexbt  7514  caucvgprprlem2  7518  suplocexprlemrl  7525  suplocexprlemmu  7526  suplocexprlemru  7527  suplocexprlemdisj  7528  suplocexprlemloc  7529  suplocexprlemex  7530  suplocexprlemub  7531  suplocexprlemlub  7532  prsrriota  7596  caucvgsrlemgt1  7603  caucvgsrlemoffres  7608  suplocsrlem  7616  rereceu  7697  recriota  7698  axarch  7699  axcaucvglemres  7707  axpre-suploclemres  7709  readdcan  7902  cnegex  7940  addcan  7942  addcan2  7943  negeu  7953  ltadd2  8181  recexre  8340  rimul  8347  ltmul1  8354  mulap0  8415  mulcanapd  8422  suprzclex  9149  qbtwnre  10034  hashcl  10527  hashen  10530  fihashdom  10549  hashunlem  10550  hashun  10551  zfz1iso  10584  cvg1nlemres  10757  cvg1n  10758  recvguniq  10767  resqrexlemoverl  10793  resqrexlemex  10797  fimaxre2  10998  climge0  11094  climrecvg1n  11117  fsum3cvg3  11165  expcnvre  11272  mertenslemub  11303  efcllem  11365  oexpneg  11574  zsupcllemex  11639  zssinfcl  11641  bezoutlemnewy  11684  bezoutlemstep  11685  dfgcd3  11698  bezout  11699  ennnfonelemex  11927  ennnfonelemrnh  11929  ennnfonelemf1  11931  ennnfonelemrn  11932  ennnfonelemdm  11933  ennnfonelemnn0  11935  ctinfomlemom  11940  ctinf  11943  ctiunctlemfo  11952  restbasg  12337  cnpnei  12388  cnptopco  12391  xmettx  12679  metcnpi3  12686  mulcncf  12760  dedekindeulemuub  12764  dedekindeulemub  12765  dedekindeulemlu  12768  dedekindicclemuub  12773  dedekindicclemub  12774  dedekindicclemlu  12777  dedekindicc  12780  ivthinclemlopn  12783  ivthinclemuopn  12785  limcimolemlt  12802  limcimo  12803  limccnp2cntop  12815  qdencn  13222  trilpolemlt1  13234