Theorem rexlimddv 2653

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ∃wrex 2509

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  disjiun  4081  nnsucpred  4713  tfrlemisucaccv  6486  tfrexlem  6495  tfr1onlemsucaccv  6502  tfrcllemsucaccv  6515  fict  7050  fidceq  7051  dif1enen  7062  php5fin  7064  fisbth  7065  fin0  7067  fin0or  7068  diffisn  7075  infnfi  7077  fidcen  7081  fientri3  7100  unsnfi  7104  unsnfidcex  7105  unsnfidcel  7106  fiuni  7168  ctmlemr  7298  ctssdccl  7301  fodjum  7336  fodju0  7337  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  cc2lem  7475  prarloclemarch2  7629  addlocpr  7746  nqprl  7761  nqpru  7762  appdiv0nq  7774  prmuloc  7776  mullocpr  7781  ltprordil  7799  ltaddpr  7807  ltexprlemopl  7811  ltexprlemopu  7813  ltexprlemloc  7817  ltexprlemrl  7820  ltexprlemru  7822  addcanprleml  7824  addcanprlemu  7825  ltaprlem  7828  ltaprg  7829  prplnqu  7830  recexprlemloc  7841  recexprlem1ssl  7843  recexprlem1ssu  7844  aptiprleml  7849  aptiprlemu  7850  ltmprr  7852  archpr  7853  cauappcvgprlemopl  7856  cauappcvgprlemopu  7858  cauappcvgprlemloc  7862  cauappcvgprlem1  7869  cauappcvgprlem2  7870  archrecpr  7874  caucvgprlemopl  7879  caucvgprlemopu  7881  caucvgprlemloc  7885  caucvgprlem2  7890  caucvgprprlemml  7904  caucvgprprlemmu  7905  caucvgprprlemopl  7907  caucvgprprlemopu  7909  caucvgprprlemloc  7913  caucvgprprlemexbt  7916  caucvgprprlem2  7920  suplocexprlemrl  7927  suplocexprlemmu  7928  suplocexprlemru  7929  suplocexprlemdisj  7930  suplocexprlemloc  7931  suplocexprlemex  7932  suplocexprlemub  7933  suplocexprlemlub  7934  prsrriota  7998  caucvgsrlemgt1  8005  caucvgsrlemoffres  8010  suplocsrlem  8018  rereceu  8099  recriota  8100  axarch  8101  axcaucvglemres  8109  axpre-suploclemres  8111  readdcan  8309  cnegex  8347  addcan  8349  addcan2  8350  negeu  8360  ltadd2  8589  recexre  8748  rimul  8755  ltmul1  8762  mulap0  8824  mulcanapd  8831  suprzclex  9568  zsupcllemex  10480  zssinfcl  10482  suprzubdc  10486  zsupssdc  10488  suprzcl2dc  10489  qbtwnre  10506  hashcl  11033  hashen  11036  fihashdom  11056  hashunlem  11057  hashun  11058  zfz1iso  11095  lencl  11107  sswrd  11112  cvg1nlemres  11536  cvg1n  11537  recvguniq  11546  resqrexlemoverl  11572  resqrexlemex  11576  fimaxre2  11778  climge0  11876  climrecvg1n  11899  fsum3cvg3  11947  expcnvre  12054  mertenslemub  12085  efcllem  12210  oexpneg  12428  bitsfzolem  12505  bitsfi  12508  bezoutlemnewy  12557  bezoutlemstep  12558  dfgcd3  12571  bezout  12572  isprm5lem  12703  ennnfonelemex  13025  ennnfonelemrnh  13027  ennnfonelemf1  13029  ennnfonelemrn  13030  ennnfonelemdm  13031  ennnfonelemnn0  13033  ctinfomlemom  13038  ctinf  13041  ctiunctlemfo  13050  nninfdclemcl  13059  nninfdc  13064  grpinvalem  13458  grprida  13460  grprcan  13610  mplsubgfilemcl  14703  restbasg  14882  cnpnei  14933  cnptopco  14936  xmettx  15224  metcnpi3  15231  mulcncf  15322  dedekindeulemuub  15331  dedekindeulemub  15332  dedekindeulemlu  15335  dedekindicclemuub  15340  dedekindicclemub  15341  dedekindicclemlu  15344  dedekindicc  15347  ivthinclemlopn  15350  ivthinclemuopn  15352  ivthreinc  15359  ivthdichlem  15365  limcimolemlt  15378  limcimo  15379  limccnp2cntop  15391  reeff1oleme  15486  eflt  15489  upgredg  15983  bj-charfunr  16341  qdencn  16567  trilpolemlt1  16581  nconstwlpolemgt0  16604