Theorem rexlimddv 2592

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2141   E.wrex 2449

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453  df-rex 2454

This theorem is referenced by:  disjiun  3982  nnsucpred  4599  tfrlemisucaccv  6302  tfrexlem  6311  tfr1onlemsucaccv  6318  tfrcllemsucaccv  6331  fict  6843  fidceq  6844  dif1enen  6855  php5fin  6857  fisbth  6858  fin0  6860  fin0or  6861  diffisn  6868  infnfi  6870  fientri3  6889  unsnfi  6893  unsnfidcex  6894  unsnfidcel  6895  fiuni  6952  ctmlemr  7082  ctssdccl  7085  fodjum  7119  fodju0  7120  exmidfodomrlemr  7168  exmidfodomrlemrALT  7169  cc2lem  7217  prarloclemarch2  7370  addlocpr  7487  nqprl  7502  nqpru  7503  appdiv0nq  7515  prmuloc  7517  mullocpr  7522  ltprordil  7540  ltaddpr  7548  ltexprlemopl  7552  ltexprlemopu  7554  ltexprlemloc  7558  ltexprlemrl  7561  ltexprlemru  7563  addcanprleml  7565  addcanprlemu  7566  ltaprlem  7569  ltaprg  7570  prplnqu  7571  recexprlemloc  7582  recexprlem1ssl  7584  recexprlem1ssu  7585  aptiprleml  7590  aptiprlemu  7591  ltmprr  7593  archpr  7594  cauappcvgprlemopl  7597  cauappcvgprlemopu  7599  cauappcvgprlemloc  7603  cauappcvgprlem1  7610  cauappcvgprlem2  7611  archrecpr  7615  caucvgprlemopl  7620  caucvgprlemopu  7622  caucvgprlemloc  7626  caucvgprlem2  7631  caucvgprprlemml  7645  caucvgprprlemmu  7646  caucvgprprlemopl  7648  caucvgprprlemopu  7650  caucvgprprlemloc  7654  caucvgprprlemexbt  7657  caucvgprprlem2  7661  suplocexprlemrl  7668  suplocexprlemmu  7669  suplocexprlemru  7670  suplocexprlemdisj  7671  suplocexprlemloc  7672  suplocexprlemex  7673  suplocexprlemub  7674  suplocexprlemlub  7675  prsrriota  7739  caucvgsrlemgt1  7746  caucvgsrlemoffres  7751  suplocsrlem  7759  rereceu  7840  recriota  7841  axarch  7842  axcaucvglemres  7850  axpre-suploclemres  7852  readdcan  8048  cnegex  8086  addcan  8088  addcan2  8089  negeu  8099  ltadd2  8327  recexre  8486  rimul  8493  ltmul1  8500  mulap0  8561  mulcanapd  8568  suprzclex  9299  qbtwnre  10202  hashcl  10704  hashen  10707  fihashdom  10727  hashunlem  10728  hashun  10729  zfz1iso  10765  cvg1nlemres  10938  cvg1n  10939  recvguniq  10948  resqrexlemoverl  10974  resqrexlemex  10978  fimaxre2  11179  climge0  11277  climrecvg1n  11300  fsum3cvg3  11348  expcnvre  11455  mertenslemub  11486  efcllem  11611  oexpneg  11825  zsupcllemex  11890  zssinfcl  11892  suprzubdc  11896  zsupssdc  11898  suprzcl2dc  11899  bezoutlemnewy  11940  bezoutlemstep  11941  dfgcd3  11954  bezout  11955  isprm5lem  12084  ennnfonelemex  12358  ennnfonelemrnh  12360  ennnfonelemf1  12362  ennnfonelemrn  12363  ennnfonelemdm  12364  ennnfonelemnn0  12366  ctinfomlemom  12371  ctinf  12374  ctiunctlemfo  12383  nninfdclemcl  12392  nninfdc  12397  grprinvlem  12628  grpridd  12630  grprcan  12729  restbasg  12923  cnpnei  12974  cnptopco  12977  xmettx  13265  metcnpi3  13272  mulcncf  13346  dedekindeulemuub  13350  dedekindeulemub  13351  dedekindeulemlu  13354  dedekindicclemuub  13359  dedekindicclemub  13360  dedekindicclemlu  13363  dedekindicc  13366  ivthinclemlopn  13369  ivthinclemuopn  13371  limcimolemlt  13388  limcimo  13389  limccnp2cntop  13401  reeff1oleme  13448  eflt  13451  bj-charfunr  13807  qdencn  14021  trilpolemlt1  14035  nconstwlpolemgt0  14057