Theorem rexlimddv 2619

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-i5r 1549

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480  df-rex 2481

This theorem is referenced by:  disjiun  4028  nnsucpred  4653  tfrlemisucaccv  6383  tfrexlem  6392  tfr1onlemsucaccv  6399  tfrcllemsucaccv  6412  fict  6929  fidceq  6930  dif1enen  6941  php5fin  6943  fisbth  6944  fin0  6946  fin0or  6947  diffisn  6954  infnfi  6956  fientri3  6976  unsnfi  6980  unsnfidcex  6981  unsnfidcel  6982  fiuni  7044  ctmlemr  7174  ctssdccl  7177  fodjum  7212  fodju0  7213  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  cc2lem  7333  prarloclemarch2  7486  addlocpr  7603  nqprl  7618  nqpru  7619  appdiv0nq  7631  prmuloc  7633  mullocpr  7638  ltprordil  7656  ltaddpr  7664  ltexprlemopl  7668  ltexprlemopu  7670  ltexprlemloc  7674  ltexprlemrl  7677  ltexprlemru  7679  addcanprleml  7681  addcanprlemu  7682  ltaprlem  7685  ltaprg  7686  prplnqu  7687  recexprlemloc  7698  recexprlem1ssl  7700  recexprlem1ssu  7701  aptiprleml  7706  aptiprlemu  7707  ltmprr  7709  archpr  7710  cauappcvgprlemopl  7713  cauappcvgprlemopu  7715  cauappcvgprlemloc  7719  cauappcvgprlem1  7726  cauappcvgprlem2  7727  archrecpr  7731  caucvgprlemopl  7736  caucvgprlemopu  7738  caucvgprlemloc  7742  caucvgprlem2  7747  caucvgprprlemml  7761  caucvgprprlemmu  7762  caucvgprprlemopl  7764  caucvgprprlemopu  7766  caucvgprprlemloc  7770  caucvgprprlemexbt  7773  caucvgprprlem2  7777  suplocexprlemrl  7784  suplocexprlemmu  7785  suplocexprlemru  7786  suplocexprlemdisj  7787  suplocexprlemloc  7788  suplocexprlemex  7789  suplocexprlemub  7790  suplocexprlemlub  7791  prsrriota  7855  caucvgsrlemgt1  7862  caucvgsrlemoffres  7867  suplocsrlem  7875  rereceu  7956  recriota  7957  axarch  7958  axcaucvglemres  7966  axpre-suploclemres  7968  readdcan  8166  cnegex  8204  addcan  8206  addcan2  8207  negeu  8217  ltadd2  8446  recexre  8605  rimul  8612  ltmul1  8619  mulap0  8681  mulcanapd  8688  suprzclex  9424  zsupcllemex  10320  zssinfcl  10322  suprzubdc  10326  zsupssdc  10328  suprzcl2dc  10329  qbtwnre  10346  hashcl  10873  hashen  10876  fihashdom  10895  hashunlem  10896  hashun  10897  zfz1iso  10933  lencl  10939  sswrd  10944  cvg1nlemres  11150  cvg1n  11151  recvguniq  11160  resqrexlemoverl  11186  resqrexlemex  11190  fimaxre2  11392  climge0  11490  climrecvg1n  11513  fsum3cvg3  11561  expcnvre  11668  mertenslemub  11699  efcllem  11824  oexpneg  12042  bitsfzolem  12118  bezoutlemnewy  12163  bezoutlemstep  12164  dfgcd3  12177  bezout  12178  isprm5lem  12309  ennnfonelemex  12631  ennnfonelemrnh  12633  ennnfonelemf1  12635  ennnfonelemrn  12636  ennnfonelemdm  12637  ennnfonelemnn0  12639  ctinfomlemom  12644  ctinf  12647  ctiunctlemfo  12656  nninfdclemcl  12665  nninfdc  12670  grpinvalem  13028  grprida  13030  grprcan  13169  restbasg  14404  cnpnei  14455  cnptopco  14458  xmettx  14746  metcnpi3  14753  mulcncf  14844  dedekindeulemuub  14853  dedekindeulemub  14854  dedekindeulemlu  14857  dedekindicclemuub  14862  dedekindicclemub  14863  dedekindicclemlu  14866  dedekindicc  14869  ivthinclemlopn  14872  ivthinclemuopn  14874  ivthreinc  14881  ivthdichlem  14887  limcimolemlt  14900  limcimo  14901  limccnp2cntop  14913  reeff1oleme  15008  eflt  15011  bj-charfunr  15456  qdencn  15671  trilpolemlt1  15685  nconstwlpolemgt0  15708