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  4078  nnsucpred  4709  tfrlemisucaccv  6477  tfrexlem  6486  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  fict  7038  fidceq  7039  dif1enen  7050  php5fin  7052  fisbth  7053  fin0  7055  fin0or  7056  diffisn  7063  infnfi  7065  fidcen  7069  fientri3  7088  unsnfi  7092  unsnfidcex  7093  unsnfidcel  7094  fiuni  7156  ctmlemr  7286  ctssdccl  7289  fodjum  7324  fodju0  7325  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  cc2lem  7463  prarloclemarch2  7617  addlocpr  7734  nqprl  7749  nqpru  7750  appdiv0nq  7762  prmuloc  7764  mullocpr  7769  ltprordil  7787  ltaddpr  7795  ltexprlemopl  7799  ltexprlemopu  7801  ltexprlemloc  7805  ltexprlemrl  7808  ltexprlemru  7810  addcanprleml  7812  addcanprlemu  7813  ltaprlem  7816  ltaprg  7817  prplnqu  7818  recexprlemloc  7829  recexprlem1ssl  7831  recexprlem1ssu  7832  aptiprleml  7837  aptiprlemu  7838  ltmprr  7840  archpr  7841  cauappcvgprlemopl  7844  cauappcvgprlemopu  7846  cauappcvgprlemloc  7850  cauappcvgprlem1  7857  cauappcvgprlem2  7858  archrecpr  7862  caucvgprlemopl  7867  caucvgprlemopu  7869  caucvgprlemloc  7873  caucvgprlem2  7878  caucvgprprlemml  7892  caucvgprprlemmu  7893  caucvgprprlemopl  7895  caucvgprprlemopu  7897  caucvgprprlemloc  7901  caucvgprprlemexbt  7904  caucvgprprlem2  7908  suplocexprlemrl  7915  suplocexprlemmu  7916  suplocexprlemru  7917  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemex  7920  suplocexprlemub  7921  suplocexprlemlub  7922  prsrriota  7986  caucvgsrlemgt1  7993  caucvgsrlemoffres  7998  suplocsrlem  8006  rereceu  8087  recriota  8088  axarch  8089  axcaucvglemres  8097  axpre-suploclemres  8099  readdcan  8297  cnegex  8335  addcan  8337  addcan2  8338  negeu  8348  ltadd2  8577  recexre  8736  rimul  8743  ltmul1  8750  mulap0  8812  mulcanapd  8819  suprzclex  9556  zsupcllemex  10462  zssinfcl  10464  suprzubdc  10468  zsupssdc  10470  suprzcl2dc  10471  qbtwnre  10488  hashcl  11015  hashen  11018  fihashdom  11037  hashunlem  11038  hashun  11039  zfz1iso  11076  lencl  11088  sswrd  11093  cvg1nlemres  11511  cvg1n  11512  recvguniq  11521  resqrexlemoverl  11547  resqrexlemex  11551  fimaxre2  11753  climge0  11851  climrecvg1n  11874  fsum3cvg3  11922  expcnvre  12029  mertenslemub  12060  efcllem  12185  oexpneg  12403  bitsfzolem  12480  bitsfi  12483  bezoutlemnewy  12532  bezoutlemstep  12533  dfgcd3  12546  bezout  12547  isprm5lem  12678  ennnfonelemex  13000  ennnfonelemrnh  13002  ennnfonelemf1  13004  ennnfonelemrn  13005  ennnfonelemdm  13006  ennnfonelemnn0  13008  ctinfomlemom  13013  ctinf  13016  ctiunctlemfo  13025  nninfdclemcl  13034  nninfdc  13039  grpinvalem  13433  grprida  13435  grprcan  13585  mplsubgfilemcl  14678  restbasg  14857  cnpnei  14908  cnptopco  14911  xmettx  15199  metcnpi3  15206  mulcncf  15297  dedekindeulemuub  15306  dedekindeulemub  15307  dedekindeulemlu  15310  dedekindicclemuub  15315  dedekindicclemub  15316  dedekindicclemlu  15319  dedekindicc  15322  ivthinclemlopn  15325  ivthinclemuopn  15327  ivthreinc  15334  ivthdichlem  15340  limcimolemlt  15353  limcimo  15354  limccnp2cntop  15366  reeff1oleme  15461  eflt  15464  upgredg  15957  bj-charfunr  16228  qdencn  16455  trilpolemlt1  16469  nconstwlpolemgt0  16492