Theorem rexlimddv 2599

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 2595	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  ∃wrex 2456

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  disjiun  3998  nnsucpred  4616  tfrlemisucaccv  6325  tfrexlem  6334  tfr1onlemsucaccv  6341  tfrcllemsucaccv  6354  fict  6867  fidceq  6868  dif1enen  6879  php5fin  6881  fisbth  6882  fin0  6884  fin0or  6885  diffisn  6892  infnfi  6894  fientri3  6913  unsnfi  6917  unsnfidcex  6918  unsnfidcel  6919  fiuni  6976  ctmlemr  7106  ctssdccl  7109  fodjum  7143  fodju0  7144  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  cc2lem  7264  prarloclemarch2  7417  addlocpr  7534  nqprl  7549  nqpru  7550  appdiv0nq  7562  prmuloc  7564  mullocpr  7569  ltprordil  7587  ltaddpr  7595  ltexprlemopl  7599  ltexprlemopu  7601  ltexprlemloc  7605  ltexprlemrl  7608  ltexprlemru  7610  addcanprleml  7612  addcanprlemu  7613  ltaprlem  7616  ltaprg  7617  prplnqu  7618  recexprlemloc  7629  recexprlem1ssl  7631  recexprlem1ssu  7632  aptiprleml  7637  aptiprlemu  7638  ltmprr  7640  archpr  7641  cauappcvgprlemopl  7644  cauappcvgprlemopu  7646  cauappcvgprlemloc  7650  cauappcvgprlem1  7657  cauappcvgprlem2  7658  archrecpr  7662  caucvgprlemopl  7667  caucvgprlemopu  7669  caucvgprlemloc  7673  caucvgprlem2  7678  caucvgprprlemml  7692  caucvgprprlemmu  7693  caucvgprprlemopl  7695  caucvgprprlemopu  7697  caucvgprprlemloc  7701  caucvgprprlemexbt  7704  caucvgprprlem2  7708  suplocexprlemrl  7715  suplocexprlemmu  7716  suplocexprlemru  7717  suplocexprlemdisj  7718  suplocexprlemloc  7719  suplocexprlemex  7720  suplocexprlemub  7721  suplocexprlemlub  7722  prsrriota  7786  caucvgsrlemgt1  7793  caucvgsrlemoffres  7798  suplocsrlem  7806  rereceu  7887  recriota  7888  axarch  7889  axcaucvglemres  7897  axpre-suploclemres  7899  readdcan  8096  cnegex  8134  addcan  8136  addcan2  8137  negeu  8147  ltadd2  8375  recexre  8534  rimul  8541  ltmul1  8548  mulap0  8610  mulcanapd  8617  suprzclex  9350  qbtwnre  10256  hashcl  10760  hashen  10763  fihashdom  10782  hashunlem  10783  hashun  10784  zfz1iso  10820  cvg1nlemres  10993  cvg1n  10994  recvguniq  11003  resqrexlemoverl  11029  resqrexlemex  11033  fimaxre2  11234  climge0  11332  climrecvg1n  11355  fsum3cvg3  11403  expcnvre  11510  mertenslemub  11541  efcllem  11666  oexpneg  11881  zsupcllemex  11946  zssinfcl  11948  suprzubdc  11952  zsupssdc  11954  suprzcl2dc  11955  bezoutlemnewy  11996  bezoutlemstep  11997  dfgcd3  12010  bezout  12011  isprm5lem  12140  ennnfonelemex  12414  ennnfonelemrnh  12416  ennnfonelemf1  12418  ennnfonelemrn  12419  ennnfonelemdm  12420  ennnfonelemnn0  12422  ctinfomlemom  12427  ctinf  12430  ctiunctlemfo  12439  nninfdclemcl  12448  nninfdc  12453  grprinvlem  12803  grpridd  12805  grprcan  12909  restbasg  13638  cnpnei  13689  cnptopco  13692  xmettx  13980  metcnpi3  13987  mulcncf  14061  dedekindeulemuub  14065  dedekindeulemub  14066  dedekindeulemlu  14069  dedekindicclemuub  14074  dedekindicclemub  14075  dedekindicclemlu  14078  dedekindicc  14081  ivthinclemlopn  14084  ivthinclemuopn  14086  limcimolemlt  14103  limcimo  14104  limccnp2cntop  14116  reeff1oleme  14163  eflt  14166  bj-charfunr  14532  qdencn  14745  trilpolemlt1  14759  nconstwlpolemgt0  14781