Theorem rexlimddv 2592

Description: Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)

Hypotheses

Ref	Expression
rexlimddv.1	⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
rexlimddv.2	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)

Assertion

Ref	Expression
rexlimddv	⊢ (𝜑 → 𝜒)

Distinct variable groups:   𝜑,𝑥   𝜒,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimddv

Step	Hyp	Ref	Expression
1		rexlimddv.1	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
2		rexlimddv.2	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)
3	2	rexlimdvaa 2588	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2141  ∃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  3984  nnsucpred  4601  tfrlemisucaccv  6304  tfrexlem  6313  tfr1onlemsucaccv  6320  tfrcllemsucaccv  6333  fict  6846  fidceq  6847  dif1enen  6858  php5fin  6860  fisbth  6861  fin0  6863  fin0or  6864  diffisn  6871  infnfi  6873  fientri3  6892  unsnfi  6896  unsnfidcex  6897  unsnfidcel  6898  fiuni  6955  ctmlemr  7085  ctssdccl  7088  fodjum  7122  fodju0  7123  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  cc2lem  7228  prarloclemarch2  7381  addlocpr  7498  nqprl  7513  nqpru  7514  appdiv0nq  7526  prmuloc  7528  mullocpr  7533  ltprordil  7551  ltaddpr  7559  ltexprlemopl  7563  ltexprlemopu  7565  ltexprlemloc  7569  ltexprlemrl  7572  ltexprlemru  7574  addcanprleml  7576  addcanprlemu  7577  ltaprlem  7580  ltaprg  7581  prplnqu  7582  recexprlemloc  7593  recexprlem1ssl  7595  recexprlem1ssu  7596  aptiprleml  7601  aptiprlemu  7602  ltmprr  7604  archpr  7605  cauappcvgprlemopl  7608  cauappcvgprlemopu  7610  cauappcvgprlemloc  7614  cauappcvgprlem1  7621  cauappcvgprlem2  7622  archrecpr  7626  caucvgprlemopl  7631  caucvgprlemopu  7633  caucvgprlemloc  7637  caucvgprlem2  7642  caucvgprprlemml  7656  caucvgprprlemmu  7657  caucvgprprlemopl  7659  caucvgprprlemopu  7661  caucvgprprlemloc  7665  caucvgprprlemexbt  7668  caucvgprprlem2  7672  suplocexprlemrl  7679  suplocexprlemmu  7680  suplocexprlemru  7681  suplocexprlemdisj  7682  suplocexprlemloc  7683  suplocexprlemex  7684  suplocexprlemub  7685  suplocexprlemlub  7686  prsrriota  7750  caucvgsrlemgt1  7757  caucvgsrlemoffres  7762  suplocsrlem  7770  rereceu  7851  recriota  7852  axarch  7853  axcaucvglemres  7861  axpre-suploclemres  7863  readdcan  8059  cnegex  8097  addcan  8099  addcan2  8100  negeu  8110  ltadd2  8338  recexre  8497  rimul  8504  ltmul1  8511  mulap0  8572  mulcanapd  8579  suprzclex  9310  qbtwnre  10213  hashcl  10715  hashen  10718  fihashdom  10738  hashunlem  10739  hashun  10740  zfz1iso  10776  cvg1nlemres  10949  cvg1n  10950  recvguniq  10959  resqrexlemoverl  10985  resqrexlemex  10989  fimaxre2  11190  climge0  11288  climrecvg1n  11311  fsum3cvg3  11359  expcnvre  11466  mertenslemub  11497  efcllem  11622  oexpneg  11836  zsupcllemex  11901  zssinfcl  11903  suprzubdc  11907  zsupssdc  11909  suprzcl2dc  11910  bezoutlemnewy  11951  bezoutlemstep  11952  dfgcd3  11965  bezout  11966  isprm5lem  12095  ennnfonelemex  12369  ennnfonelemrnh  12371  ennnfonelemf1  12373  ennnfonelemrn  12374  ennnfonelemdm  12375  ennnfonelemnn0  12377  ctinfomlemom  12382  ctinf  12385  ctiunctlemfo  12394  nninfdclemcl  12403  nninfdc  12408  grprinvlem  12639  grpridd  12641  grprcan  12740  restbasg  12962  cnpnei  13013  cnptopco  13016  xmettx  13304  metcnpi3  13311  mulcncf  13385  dedekindeulemuub  13389  dedekindeulemub  13390  dedekindeulemlu  13393  dedekindicclemuub  13398  dedekindicclemub  13399  dedekindicclemlu  13402  dedekindicc  13405  ivthinclemlopn  13408  ivthinclemuopn  13410  limcimolemlt  13427  limcimo  13428  limccnp2cntop  13440  reeff1oleme  13487  eflt  13490  bj-charfunr  13845  qdencn  14059  trilpolemlt1  14073  nconstwlpolemgt0  14095