Theorem rexlimddv 2616

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-i5r 1546

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477  df-rex 2478

This theorem is referenced by:  disjiun  4025  nnsucpred  4650  tfrlemisucaccv  6380  tfrexlem  6389  tfr1onlemsucaccv  6396  tfrcllemsucaccv  6409  fict  6926  fidceq  6927  dif1enen  6938  php5fin  6940  fisbth  6941  fin0  6943  fin0or  6944  diffisn  6951  infnfi  6953  fientri3  6973  unsnfi  6977  unsnfidcex  6978  unsnfidcel  6979  fiuni  7039  ctmlemr  7169  ctssdccl  7172  fodjum  7207  fodju0  7208  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  cc2lem  7328  prarloclemarch2  7481  addlocpr  7598  nqprl  7613  nqpru  7614  appdiv0nq  7626  prmuloc  7628  mullocpr  7633  ltprordil  7651  ltaddpr  7659  ltexprlemopl  7663  ltexprlemopu  7665  ltexprlemloc  7669  ltexprlemrl  7672  ltexprlemru  7674  addcanprleml  7676  addcanprlemu  7677  ltaprlem  7680  ltaprg  7681  prplnqu  7682  recexprlemloc  7693  recexprlem1ssl  7695  recexprlem1ssu  7696  aptiprleml  7701  aptiprlemu  7702  ltmprr  7704  archpr  7705  cauappcvgprlemopl  7708  cauappcvgprlemopu  7710  cauappcvgprlemloc  7714  cauappcvgprlem1  7721  cauappcvgprlem2  7722  archrecpr  7726  caucvgprlemopl  7731  caucvgprlemopu  7733  caucvgprlemloc  7737  caucvgprlem2  7742  caucvgprprlemml  7756  caucvgprprlemmu  7757  caucvgprprlemopl  7759  caucvgprprlemopu  7761  caucvgprprlemloc  7765  caucvgprprlemexbt  7768  caucvgprprlem2  7772  suplocexprlemrl  7779  suplocexprlemmu  7780  suplocexprlemru  7781  suplocexprlemdisj  7782  suplocexprlemloc  7783  suplocexprlemex  7784  suplocexprlemub  7785  suplocexprlemlub  7786  prsrriota  7850  caucvgsrlemgt1  7857  caucvgsrlemoffres  7862  suplocsrlem  7870  rereceu  7951  recriota  7952  axarch  7953  axcaucvglemres  7961  axpre-suploclemres  7963  readdcan  8161  cnegex  8199  addcan  8201  addcan2  8202  negeu  8212  ltadd2  8440  recexre  8599  rimul  8606  ltmul1  8613  mulap0  8675  mulcanapd  8682  suprzclex  9418  qbtwnre  10328  hashcl  10855  hashen  10858  fihashdom  10877  hashunlem  10878  hashun  10879  zfz1iso  10915  lencl  10921  sswrd  10926  cvg1nlemres  11132  cvg1n  11133  recvguniq  11142  resqrexlemoverl  11168  resqrexlemex  11172  fimaxre2  11373  climge0  11471  climrecvg1n  11494  fsum3cvg3  11542  expcnvre  11649  mertenslemub  11680  efcllem  11805  oexpneg  12021  zsupcllemex  12086  zssinfcl  12088  suprzubdc  12092  zsupssdc  12094  suprzcl2dc  12095  bezoutlemnewy  12136  bezoutlemstep  12137  dfgcd3  12150  bezout  12151  isprm5lem  12282  ennnfonelemex  12574  ennnfonelemrnh  12576  ennnfonelemf1  12578  ennnfonelemrn  12579  ennnfonelemdm  12580  ennnfonelemnn0  12582  ctinfomlemom  12587  ctinf  12590  ctiunctlemfo  12599  nninfdclemcl  12608  nninfdc  12613  grpinvalem  12971  grprida  12973  grprcan  13112  restbasg  14347  cnpnei  14398  cnptopco  14401  xmettx  14689  metcnpi3  14696  mulcncf  14787  dedekindeulemuub  14796  dedekindeulemub  14797  dedekindeulemlu  14800  dedekindicclemuub  14805  dedekindicclemub  14806  dedekindicclemlu  14809  dedekindicc  14812  ivthinclemlopn  14815  ivthinclemuopn  14817  ivthreinc  14824  ivthdichlem  14830  limcimolemlt  14843  limcimo  14844  limccnp2cntop  14856  reeff1oleme  14948  eflt  14951  bj-charfunr  15372  qdencn  15587  trilpolemlt1  15601  nconstwlpolemgt0  15624