Theorem rexlimddv 2653

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

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  disjiun  4078  nnsucpred  4709  tfrlemisucaccv  6477  tfrexlem  6486  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  fict  7038  fidceq  7039  dif1enen  7050  php5fin  7052  fisbth  7053  fin0  7055  fin0or  7056  diffisn  7063  infnfi  7065  fidcen  7069  fientri3  7088  unsnfi  7092  unsnfidcex  7093  unsnfidcel  7094  fiuni  7156  ctmlemr  7286  ctssdccl  7289  fodjum  7324  fodju0  7325  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  cc2lem  7463  prarloclemarch2  7617  addlocpr  7734  nqprl  7749  nqpru  7750  appdiv0nq  7762  prmuloc  7764  mullocpr  7769  ltprordil  7787  ltaddpr  7795  ltexprlemopl  7799  ltexprlemopu  7801  ltexprlemloc  7805  ltexprlemrl  7808  ltexprlemru  7810  addcanprleml  7812  addcanprlemu  7813  ltaprlem  7816  ltaprg  7817  prplnqu  7818  recexprlemloc  7829  recexprlem1ssl  7831  recexprlem1ssu  7832  aptiprleml  7837  aptiprlemu  7838  ltmprr  7840  archpr  7841  cauappcvgprlemopl  7844  cauappcvgprlemopu  7846  cauappcvgprlemloc  7850  cauappcvgprlem1  7857  cauappcvgprlem2  7858  archrecpr  7862  caucvgprlemopl  7867  caucvgprlemopu  7869  caucvgprlemloc  7873  caucvgprlem2  7878  caucvgprprlemml  7892  caucvgprprlemmu  7893  caucvgprprlemopl  7895  caucvgprprlemopu  7897  caucvgprprlemloc  7901  caucvgprprlemexbt  7904  caucvgprprlem2  7908  suplocexprlemrl  7915  suplocexprlemmu  7916  suplocexprlemru  7917  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemex  7920  suplocexprlemub  7921  suplocexprlemlub  7922  prsrriota  7986  caucvgsrlemgt1  7993  caucvgsrlemoffres  7998  suplocsrlem  8006  rereceu  8087  recriota  8088  axarch  8089  axcaucvglemres  8097  axpre-suploclemres  8099  readdcan  8297  cnegex  8335  addcan  8337  addcan2  8338  negeu  8348  ltadd2  8577  recexre  8736  rimul  8743  ltmul1  8750  mulap0  8812  mulcanapd  8819  suprzclex  9556  zsupcllemex  10462  zssinfcl  10464  suprzubdc  10468  zsupssdc  10470  suprzcl2dc  10471  qbtwnre  10488  hashcl  11015  hashen  11018  fihashdom  11037  hashunlem  11038  hashun  11039  zfz1iso  11076  lencl  11088  sswrd  11093  cvg1nlemres  11512  cvg1n  11513  recvguniq  11522  resqrexlemoverl  11548  resqrexlemex  11552  fimaxre2  11754  climge0  11852  climrecvg1n  11875  fsum3cvg3  11923  expcnvre  12030  mertenslemub  12061  efcllem  12186  oexpneg  12404  bitsfzolem  12481  bitsfi  12484  bezoutlemnewy  12533  bezoutlemstep  12534  dfgcd3  12547  bezout  12548  isprm5lem  12679  ennnfonelemex  13001  ennnfonelemrnh  13003  ennnfonelemf1  13005  ennnfonelemrn  13006  ennnfonelemdm  13007  ennnfonelemnn0  13009  ctinfomlemom  13014  ctinf  13017  ctiunctlemfo  13026  nninfdclemcl  13035  nninfdc  13040  grpinvalem  13434  grprida  13436  grprcan  13586  mplsubgfilemcl  14679  restbasg  14858  cnpnei  14909  cnptopco  14912  xmettx  15200  metcnpi3  15207  mulcncf  15298  dedekindeulemuub  15307  dedekindeulemub  15308  dedekindeulemlu  15311  dedekindicclemuub  15316  dedekindicclemub  15317  dedekindicclemlu  15320  dedekindicc  15323  ivthinclemlopn  15326  ivthinclemuopn  15328  ivthreinc  15335  ivthdichlem  15341  limcimolemlt  15354  limcimo  15355  limccnp2cntop  15367  reeff1oleme  15462  eflt  15465  upgredg  15958  bj-charfunr  16256  qdencn  16483  trilpolemlt1  16497  nconstwlpolemgt0  16520