Theorem rexlimddv 2628

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

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-i5r 1558

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489  df-rex 2490

This theorem is referenced by:  disjiun  4040  nnsucpred  4666  tfrlemisucaccv  6413  tfrexlem  6422  tfr1onlemsucaccv  6429  tfrcllemsucaccv  6442  fict  6967  fidceq  6968  dif1enen  6979  php5fin  6981  fisbth  6982  fin0  6984  fin0or  6985  diffisn  6992  infnfi  6994  fientri3  7014  unsnfi  7018  unsnfidcex  7019  unsnfidcel  7020  fiuni  7082  ctmlemr  7212  ctssdccl  7215  fodjum  7250  fodju0  7251  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  cc2lem  7380  prarloclemarch2  7534  addlocpr  7651  nqprl  7666  nqpru  7667  appdiv0nq  7679  prmuloc  7681  mullocpr  7686  ltprordil  7704  ltaddpr  7712  ltexprlemopl  7716  ltexprlemopu  7718  ltexprlemloc  7722  ltexprlemrl  7725  ltexprlemru  7727  addcanprleml  7729  addcanprlemu  7730  ltaprlem  7733  ltaprg  7734  prplnqu  7735  recexprlemloc  7746  recexprlem1ssl  7748  recexprlem1ssu  7749  aptiprleml  7754  aptiprlemu  7755  ltmprr  7757  archpr  7758  cauappcvgprlemopl  7761  cauappcvgprlemopu  7763  cauappcvgprlemloc  7767  cauappcvgprlem1  7774  cauappcvgprlem2  7775  archrecpr  7779  caucvgprlemopl  7784  caucvgprlemopu  7786  caucvgprlemloc  7790  caucvgprlem2  7795  caucvgprprlemml  7809  caucvgprprlemmu  7810  caucvgprprlemopl  7812  caucvgprprlemopu  7814  caucvgprprlemloc  7818  caucvgprprlemexbt  7821  caucvgprprlem2  7825  suplocexprlemrl  7832  suplocexprlemmu  7833  suplocexprlemru  7834  suplocexprlemdisj  7835  suplocexprlemloc  7836  suplocexprlemex  7837  suplocexprlemub  7838  suplocexprlemlub  7839  prsrriota  7903  caucvgsrlemgt1  7910  caucvgsrlemoffres  7915  suplocsrlem  7923  rereceu  8004  recriota  8005  axarch  8006  axcaucvglemres  8014  axpre-suploclemres  8016  readdcan  8214  cnegex  8252  addcan  8254  addcan2  8255  negeu  8265  ltadd2  8494  recexre  8653  rimul  8660  ltmul1  8667  mulap0  8729  mulcanapd  8736  suprzclex  9473  zsupcllemex  10375  zssinfcl  10377  suprzubdc  10381  zsupssdc  10383  suprzcl2dc  10384  qbtwnre  10401  hashcl  10928  hashen  10931  fihashdom  10950  hashunlem  10951  hashun  10952  zfz1iso  10988  lencl  11000  sswrd  11005  cvg1nlemres  11329  cvg1n  11330  recvguniq  11339  resqrexlemoverl  11365  resqrexlemex  11369  fimaxre2  11571  climge0  11669  climrecvg1n  11692  fsum3cvg3  11740  expcnvre  11847  mertenslemub  11878  efcllem  12003  oexpneg  12221  bitsfzolem  12298  bitsfi  12301  bezoutlemnewy  12350  bezoutlemstep  12351  dfgcd3  12364  bezout  12365  isprm5lem  12496  ennnfonelemex  12818  ennnfonelemrnh  12820  ennnfonelemf1  12822  ennnfonelemrn  12823  ennnfonelemdm  12824  ennnfonelemnn0  12826  ctinfomlemom  12831  ctinf  12834  ctiunctlemfo  12843  nninfdclemcl  12852  nninfdc  12857  grpinvalem  13250  grprida  13252  grprcan  13402  mplsubgfilemcl  14494  restbasg  14673  cnpnei  14724  cnptopco  14727  xmettx  15015  metcnpi3  15022  mulcncf  15113  dedekindeulemuub  15122  dedekindeulemub  15123  dedekindeulemlu  15126  dedekindicclemuub  15131  dedekindicclemub  15132  dedekindicclemlu  15135  dedekindicc  15138  ivthinclemlopn  15141  ivthinclemuopn  15143  ivthreinc  15150  ivthdichlem  15156  limcimolemlt  15169  limcimo  15170  limccnp2cntop  15182  reeff1oleme  15277  eflt  15280  bj-charfunr  15783  qdencn  16003  trilpolemlt1  16017  nconstwlpolemgt0  16040