Theorem rexlimddv 2673

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   E.wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is used by:  disjiun  4125  nnsucpred  4764  tfrlemisucaccv  6596  tfrexlem  6605  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  fict  7170  fidceq  7171  dif1enen  7184  php5fin  7186  fisbth  7187  fin0  7189  fin0or  7190  diffisn  7197  infnfi  7199  fidcen  7203  fientri3  7222  unsnfi  7226  unsnfidcex  7227  unsnfidcel  7228  fiuni  7312  ctmlemr  7448  ctssdccl  7451  fodjum  7486  fodju0  7487  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  cc2lem  7632  prarloclemarch2  7786  addlocpr  7903  nqprl  7918  nqpru  7919  appdiv0nq  7931  prmuloc  7933  mullocpr  7938  ltprordil  7956  ltaddpr  7964  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemloc  7974  ltexprlemrl  7977  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  ltaprlem  7985  ltaprg  7986  prplnqu  7987  recexprlemloc  7998  recexprlem1ssl  8000  recexprlem1ssu  8001  aptiprleml  8006  aptiprlemu  8007  ltmprr  8009  archpr  8010  cauappcvgprlemopl  8013  cauappcvgprlemopu  8015  cauappcvgprlemloc  8019  cauappcvgprlem1  8026  cauappcvgprlem2  8027  archrecpr  8031  caucvgprlemopl  8036  caucvgprlemopu  8038  caucvgprlemloc  8042  caucvgprlem2  8047  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemopu  8066  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  caucvgprprlem2  8077  suplocexprlemrl  8084  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemex  8089  suplocexprlemub  8090  suplocexprlemlub  8091  prsrriota  8155  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  suplocsrlem  8175  rereceu  8256  recriota  8257  axarch  8258  axcaucvglemres  8266  axpre-suploclemres  8268  readdcan  8467  cnegex  8505  addcan  8507  addcan2  8508  negeu  8518  ltadd2  8748  recexre  8908  rimul  8915  ltmul1  8922  mulap0  8984  mulcanapd  8991  suprzclex  9748  zsupcllemex  10673  zssinfcl  10675  suprzubdc  10681  zsupssdc  10683  suprzcl2dc  10684  qbtwnre  10701  hashcl  11234  hashen  11237  fihashdom  11257  hashunlem  11258  hashun  11259  zfz1iso  11307  lencl  11322  sswrd  11327  cvg1nlemres  11765  cvg1n  11766  recvguniq  11775  resqrexlemoverl  11801  resqrexlemex  11805  fimaxre2  12008  climge0  12107  climrecvg1n  12130  fsum3cvg3  12179  expcnvre  12286  mertenslemub  12317  efcllem  12442  oexpneg  12660  bitsfzolem  12737  bitsfi  12740  bezoutlemnewy  12789  bezoutlemstep  12790  dfgcd3  12803  bezout  12804  isprm5lem  12936  ballotfilemscl  13296  ballotfilemsle  13297  ennnfonelemex  13354  ennnfonelemrnh  13356  ennnfonelemf1  13358  ennnfonelemrn  13359  ennnfonelemdm  13360  ennnfonelemnn0  13362  ctinfomlemom  13367  ctinf  13370  ctiunctlemfo  13379  nninfdclemcl  13388  nninfdc  13393  grpinvalem  13754  grprida  13756  grprcan  13891  mplsubgfilemcl  15139  restbasg  15318  cnpnei  15369  cnptopco  15372  xmettx  15660  metcnpi3  15667  mulcncf  15758  dedekindeulemuub  15767  dedekindeulemub  15768  dedekindeulemlu  15771  dedekindicclemuub  15776  dedekindicclemub  15777  dedekindicclemlu  15780  dedekindicc  15783  ivthinclemlopn  15786  ivthinclemuopn  15788  ivthreinc  15795  ivthdichlem  15801  limcimolemlt  15814  limcimo  15815  limccnp2cntop  15827  reeff1oleme  15922  eflt  15925  upgredg  16483  bj-charfunr  16934  qdencn  17170  trilpolemlt1  17188  nconstwlpolemgt0  17212