Theorem rexlimddv 2507

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-4 1452  ax-17 1471  ax-ial 1479  ax-i5r 1480

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-ral 2375  df-rex 2376

This theorem is referenced by:  disjiun  3862  grprinvlem  5877  grpridd  5879  tfrlemisucaccv  6128  tfrexlem  6137  tfr1onlemsucaccv  6144  tfrcllemsucaccv  6157  fict  6664  fidceq  6665  dif1enen  6676  php5fin  6678  fisbth  6679  fin0  6681  fin0or  6682  diffisn  6689  infnfi  6691  fientri3  6705  unsnfi  6709  unsnfidcex  6710  unsnfidcel  6711  ctmlemr  6870  fodjum  6889  fodju0  6890  exmidfodomrlemr  6925  exmidfodomrlemrALT  6926  prarloclemarch2  7075  addlocpr  7192  nqprl  7207  nqpru  7208  appdiv0nq  7220  prmuloc  7222  mullocpr  7227  ltprordil  7245  ltaddpr  7253  ltexprlemopl  7257  ltexprlemopu  7259  ltexprlemloc  7263  ltexprlemrl  7266  ltexprlemru  7268  addcanprleml  7270  addcanprlemu  7271  ltaprlem  7274  ltaprg  7275  prplnqu  7276  recexprlemloc  7287  recexprlem1ssl  7289  recexprlem1ssu  7290  aptiprleml  7295  aptiprlemu  7296  ltmprr  7298  archpr  7299  cauappcvgprlemopl  7302  cauappcvgprlemopu  7304  cauappcvgprlemloc  7308  cauappcvgprlem1  7315  cauappcvgprlem2  7316  archrecpr  7320  caucvgprlemopl  7325  caucvgprlemopu  7327  caucvgprlemloc  7331  caucvgprlem2  7336  caucvgprprlemml  7350  caucvgprprlemmu  7351  caucvgprprlemopl  7353  caucvgprprlemopu  7355  caucvgprprlemloc  7359  caucvgprprlemexbt  7362  caucvgprprlem2  7366  prsrriota  7430  caucvgsrlemgt1  7437  caucvgsrlemoffres  7442  rereceu  7521  recriota  7522  axarch  7523  axcaucvglemres  7531  readdcan  7719  cnegex  7757  addcan  7759  addcan2  7760  negeu  7770  ltadd2  7994  recexre  8152  rimul  8159  ltmul1  8166  mulap0  8220  mulcanapd  8227  suprzclex  8943  qbtwnre  9817  hashcl  10320  hashen  10323  fihashdom  10342  hashunlem  10343  hashun  10344  zfz1iso  10377  cvg1nlemres  10549  cvg1n  10550  recvguniq  10559  resqrexlemoverl  10585  resqrexlemex  10589  fimaxre2  10789  climge0  10884  climrecvg1n  10907  fsum3cvg3  10955  expcnvre  11062  mertenslemub  11093  efcllem  11114  oexpneg  11320  zsupcllemex  11385  zssinfcl  11387  bezoutlemnewy  11428  bezoutlemstep  11429  dfgcd3  11442  bezout  11443  restbasg  12036  cnpnei  12086  cnptopco  12089  metcnpi3  12315  mulcncf  12370  nnsucpred  12612  qdencn  12636