Theorem rexlimddv 2655

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

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515  df-rex 2516

This theorem is referenced by:  disjiun  4083  nnsucpred  4715  tfrlemisucaccv  6491  tfrexlem  6500  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  fict  7055  fidceq  7056  dif1enen  7069  php5fin  7071  fisbth  7072  fin0  7074  fin0or  7075  diffisn  7082  infnfi  7084  fidcen  7088  fientri3  7107  unsnfi  7111  unsnfidcex  7112  unsnfidcel  7113  fiuni  7177  ctmlemr  7307  ctssdccl  7310  fodjum  7345  fodju0  7346  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  cc2lem  7485  prarloclemarch2  7639  addlocpr  7756  nqprl  7771  nqpru  7772  appdiv0nq  7784  prmuloc  7786  mullocpr  7791  ltprordil  7809  ltaddpr  7817  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemloc  7827  ltexprlemrl  7830  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  ltaprlem  7838  ltaprg  7839  prplnqu  7840  recexprlemloc  7851  recexprlem1ssl  7853  recexprlem1ssu  7854  aptiprleml  7859  aptiprlemu  7860  ltmprr  7862  archpr  7863  cauappcvgprlemopl  7866  cauappcvgprlemopu  7868  cauappcvgprlemloc  7872  cauappcvgprlem1  7879  cauappcvgprlem2  7880  archrecpr  7884  caucvgprlemopl  7889  caucvgprlemopu  7891  caucvgprlemloc  7895  caucvgprlem2  7900  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemopu  7919  caucvgprprlemloc  7923  caucvgprprlemexbt  7926  caucvgprprlem2  7930  suplocexprlemrl  7937  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemex  7942  suplocexprlemub  7943  suplocexprlemlub  7944  prsrriota  8008  caucvgsrlemgt1  8015  caucvgsrlemoffres  8020  suplocsrlem  8028  rereceu  8109  recriota  8110  axarch  8111  axcaucvglemres  8119  axpre-suploclemres  8121  readdcan  8319  cnegex  8357  addcan  8359  addcan2  8360  negeu  8370  ltadd2  8599  recexre  8758  rimul  8765  ltmul1  8772  mulap0  8834  mulcanapd  8841  suprzclex  9578  zsupcllemex  10491  zssinfcl  10493  suprzubdc  10497  zsupssdc  10499  suprzcl2dc  10500  qbtwnre  10517  hashcl  11044  hashen  11047  fihashdom  11067  hashunlem  11068  hashun  11069  zfz1iso  11106  lencl  11121  sswrd  11126  cvg1nlemres  11563  cvg1n  11564  recvguniq  11573  resqrexlemoverl  11599  resqrexlemex  11603  fimaxre2  11805  climge0  11903  climrecvg1n  11926  fsum3cvg3  11975  expcnvre  12082  mertenslemub  12113  efcllem  12238  oexpneg  12456  bitsfzolem  12533  bitsfi  12536  bezoutlemnewy  12585  bezoutlemstep  12586  dfgcd3  12599  bezout  12600  isprm5lem  12731  ennnfonelemex  13053  ennnfonelemrnh  13055  ennnfonelemf1  13057  ennnfonelemrn  13058  ennnfonelemdm  13059  ennnfonelemnn0  13061  ctinfomlemom  13066  ctinf  13069  ctiunctlemfo  13078  nninfdclemcl  13087  nninfdc  13092  grpinvalem  13486  grprida  13488  grprcan  13638  mplsubgfilemcl  14732  restbasg  14911  cnpnei  14962  cnptopco  14965  xmettx  15253  metcnpi3  15260  mulcncf  15351  dedekindeulemuub  15360  dedekindeulemub  15361  dedekindeulemlu  15364  dedekindicclemuub  15369  dedekindicclemub  15370  dedekindicclemlu  15373  dedekindicc  15376  ivthinclemlopn  15379  ivthinclemuopn  15381  ivthreinc  15388  ivthdichlem  15394  limcimolemlt  15407  limcimo  15408  limccnp2cntop  15420  reeff1oleme  15515  eflt  15518  upgredg  16014  bj-charfunr  16456  qdencn  16682  trilpolemlt1  16696  nconstwlpolemgt0  16720