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  4766  tfrlemisucaccv  6600  tfrexlem  6609  tfr1onlemsucaccv  6616  tfrcllemsucaccv  6629  fict  7174  fidceq  7175  dif1enen  7188  php5fin  7190  fisbth  7191  fin0  7193  fin0or  7194  diffisn  7201  infnfi  7203  fidcen  7207  fientri3  7226  unsnfi  7230  unsnfidcex  7231  unsnfidcel  7232  fiuni  7317  ctmlemr  7454  ctssdccl  7457  fodjum  7492  fodju0  7493  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  cc2lem  7638  prarloclemarch2  7792  addlocpr  7909  nqprl  7924  nqpru  7925  appdiv0nq  7937  prmuloc  7939  mullocpr  7944  ltprordil  7962  ltaddpr  7970  ltexprlemopl  7974  ltexprlemopu  7976  ltexprlemloc  7980  ltexprlemrl  7983  ltexprlemru  7985  addcanprleml  7987  addcanprlemu  7988  ltaprlem  7991  ltaprg  7992  prplnqu  7993  recexprlemloc  8004  recexprlem1ssl  8006  recexprlem1ssu  8007  aptiprleml  8012  aptiprlemu  8013  ltmprr  8015  archpr  8016  cauappcvgprlemopl  8019  cauappcvgprlemopu  8021  cauappcvgprlemloc  8025  cauappcvgprlem1  8032  cauappcvgprlem2  8033  archrecpr  8037  caucvgprlemopl  8042  caucvgprlemopu  8044  caucvgprlemloc  8048  caucvgprlem2  8053  caucvgprprlemml  8067  caucvgprprlemmu  8068  caucvgprprlemopl  8070  caucvgprprlemopu  8072  caucvgprprlemloc  8076  caucvgprprlemexbt  8079  caucvgprprlem2  8083  suplocexprlemrl  8090  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemex  8095  suplocexprlemub  8096  suplocexprlemlub  8097  prsrriota  8161  caucvgsrlemgt1  8168  caucvgsrlemoffres  8173  suplocsrlem  8181  rereceu  8262  recriota  8263  axarch  8264  axcaucvglemres  8272  axpre-suploclemres  8274  readdcan  8473  cnegex  8511  addcan  8513  addcan2  8514  negeu  8524  ltadd2  8754  recexre  8914  rimul  8921  ltmul1  8928  mulap0  8990  mulcanapd  8997  suprzclex  9755  zsupcllemex  10680  zssinfcl  10682  suprzubdc  10688  zsupssdc  10690  suprzcl2dc  10691  qbtwnre  10708  hashcl  11242  hashen  11245  fihashdom  11265  hashunlem  11266  hashun  11267  zfz1iso  11315  lencl  11330  sswrd  11335  cvg1nlemres  11773  cvg1n  11774  recvguniq  11783  resqrexlemoverl  11809  resqrexlemex  11813  fimaxre2  12016  climge0  12116  climrecvg1n  12139  fsum3cvg3  12188  expcnvre  12295  mertenslemub  12326  efcllem  12451  oexpneg  12669  bitsfzolem  12746  bitsfi  12749  bezoutlemnewy  12798  bezoutlemstep  12799  dfgcd3  12812  bezout  12813  isprm5lem  12945  ballotfilemscl  13305  ballotfilemsle  13306  ennnfonelemex  13363  ennnfonelemrnh  13365  ennnfonelemf1  13367  ennnfonelemrn  13368  ennnfonelemdm  13369  ennnfonelemnn0  13371  ctinfomlemom  13376  ctinf  13379  ctiunctlemfo  13388  nninfdclemcl  13397  nninfdc  13402  grpinvalem  13764  grprida  13766  grprcan  13901  psrbaglefifi  15172  mplsubgfilemcl  15215  restbasg  15394  cnpnei  15445  cnptopco  15448  xmettx  15736  metcnpi3  15743  mulcncf  15834  dedekindeulemuub  15843  dedekindeulemub  15844  dedekindeulemlu  15847  dedekindicclemuub  15852  dedekindicclemub  15853  dedekindicclemlu  15856  dedekindicc  15859  ivthinclemlopn  15862  ivthinclemuopn  15864  ivthreinc  15871  ivthdichlem  15877  limcimolemlt  15890  limcimo  15891  limccnp2cntop  15903  reeff1oleme  15998  eflt  16001  upgredg  16590  bj-charfunr  17041  qdencn  17278  trilpolemlt1  17297  nconstwlpolemgt0  17321