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  4024  nnsucpred  4649  tfrlemisucaccv  6378  tfrexlem  6387  tfr1onlemsucaccv  6394  tfrcllemsucaccv  6407  fict  6924  fidceq  6925  dif1enen  6936  php5fin  6938  fisbth  6939  fin0  6941  fin0or  6942  diffisn  6949  infnfi  6951  fientri3  6971  unsnfi  6975  unsnfidcex  6976  unsnfidcel  6977  fiuni  7037  ctmlemr  7167  ctssdccl  7170  fodjum  7205  fodju0  7206  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  cc2lem  7326  prarloclemarch2  7479  addlocpr  7596  nqprl  7611  nqpru  7612  appdiv0nq  7624  prmuloc  7626  mullocpr  7631  ltprordil  7649  ltaddpr  7657  ltexprlemopl  7661  ltexprlemopu  7663  ltexprlemloc  7667  ltexprlemrl  7670  ltexprlemru  7672  addcanprleml  7674  addcanprlemu  7675  ltaprlem  7678  ltaprg  7679  prplnqu  7680  recexprlemloc  7691  recexprlem1ssl  7693  recexprlem1ssu  7694  aptiprleml  7699  aptiprlemu  7700  ltmprr  7702  archpr  7703  cauappcvgprlemopl  7706  cauappcvgprlemopu  7708  cauappcvgprlemloc  7712  cauappcvgprlem1  7719  cauappcvgprlem2  7720  archrecpr  7724  caucvgprlemopl  7729  caucvgprlemopu  7731  caucvgprlemloc  7735  caucvgprlem2  7740  caucvgprprlemml  7754  caucvgprprlemmu  7755  caucvgprprlemopl  7757  caucvgprprlemopu  7759  caucvgprprlemloc  7763  caucvgprprlemexbt  7766  caucvgprprlem2  7770  suplocexprlemrl  7777  suplocexprlemmu  7778  suplocexprlemru  7779  suplocexprlemdisj  7780  suplocexprlemloc  7781  suplocexprlemex  7782  suplocexprlemub  7783  suplocexprlemlub  7784  prsrriota  7848  caucvgsrlemgt1  7855  caucvgsrlemoffres  7860  suplocsrlem  7868  rereceu  7949  recriota  7950  axarch  7951  axcaucvglemres  7959  axpre-suploclemres  7961  readdcan  8159  cnegex  8197  addcan  8199  addcan2  8200  negeu  8210  ltadd2  8438  recexre  8597  rimul  8604  ltmul1  8611  mulap0  8673  mulcanapd  8680  suprzclex  9415  qbtwnre  10325  hashcl  10852  hashen  10855  fihashdom  10874  hashunlem  10875  hashun  10876  zfz1iso  10912  lencl  10918  sswrd  10923  cvg1nlemres  11129  cvg1n  11130  recvguniq  11139  resqrexlemoverl  11165  resqrexlemex  11169  fimaxre2  11370  climge0  11468  climrecvg1n  11491  fsum3cvg3  11539  expcnvre  11646  mertenslemub  11677  efcllem  11802  oexpneg  12018  zsupcllemex  12083  zssinfcl  12085  suprzubdc  12089  zsupssdc  12091  suprzcl2dc  12092  bezoutlemnewy  12133  bezoutlemstep  12134  dfgcd3  12147  bezout  12148  isprm5lem  12279  ennnfonelemex  12571  ennnfonelemrnh  12573  ennnfonelemf1  12575  ennnfonelemrn  12576  ennnfonelemdm  12577  ennnfonelemnn0  12579  ctinfomlemom  12584  ctinf  12587  ctiunctlemfo  12596  nninfdclemcl  12605  nninfdc  12610  grpinvalem  12968  grprida  12970  grprcan  13109  restbasg  14336  cnpnei  14387  cnptopco  14390  xmettx  14678  metcnpi3  14685  mulcncf  14762  dedekindeulemuub  14771  dedekindeulemub  14772  dedekindeulemlu  14775  dedekindicclemuub  14780  dedekindicclemub  14781  dedekindicclemlu  14784  dedekindicc  14787  ivthinclemlopn  14790  ivthinclemuopn  14792  ivthreinc  14799  ivthdichlem  14805  limcimolemlt  14818  limcimo  14819  limccnp2cntop  14831  reeff1oleme  14907  eflt  14910  bj-charfunr  15302  qdencn  15517  trilpolemlt1  15531  nconstwlpolemgt0  15554