Theorem rexlimddv 2619

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  ∃wrex 2476

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-i5r 1549

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480  df-rex 2481

This theorem is referenced by:  disjiun  4029  nnsucpred  4654  tfrlemisucaccv  6392  tfrexlem  6401  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  fict  6938  fidceq  6939  dif1enen  6950  php5fin  6952  fisbth  6953  fin0  6955  fin0or  6956  diffisn  6963  infnfi  6965  fientri3  6985  unsnfi  6989  unsnfidcex  6990  unsnfidcel  6991  fiuni  7053  ctmlemr  7183  ctssdccl  7186  fodjum  7221  fodju0  7222  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  cc2lem  7349  prarloclemarch2  7503  addlocpr  7620  nqprl  7635  nqpru  7636  appdiv0nq  7648  prmuloc  7650  mullocpr  7655  ltprordil  7673  ltaddpr  7681  ltexprlemopl  7685  ltexprlemopu  7687  ltexprlemloc  7691  ltexprlemrl  7694  ltexprlemru  7696  addcanprleml  7698  addcanprlemu  7699  ltaprlem  7702  ltaprg  7703  prplnqu  7704  recexprlemloc  7715  recexprlem1ssl  7717  recexprlem1ssu  7718  aptiprleml  7723  aptiprlemu  7724  ltmprr  7726  archpr  7727  cauappcvgprlemopl  7730  cauappcvgprlemopu  7732  cauappcvgprlemloc  7736  cauappcvgprlem1  7743  cauappcvgprlem2  7744  archrecpr  7748  caucvgprlemopl  7753  caucvgprlemopu  7755  caucvgprlemloc  7759  caucvgprlem2  7764  caucvgprprlemml  7778  caucvgprprlemmu  7779  caucvgprprlemopl  7781  caucvgprprlemopu  7783  caucvgprprlemloc  7787  caucvgprprlemexbt  7790  caucvgprprlem2  7794  suplocexprlemrl  7801  suplocexprlemmu  7802  suplocexprlemru  7803  suplocexprlemdisj  7804  suplocexprlemloc  7805  suplocexprlemex  7806  suplocexprlemub  7807  suplocexprlemlub  7808  prsrriota  7872  caucvgsrlemgt1  7879  caucvgsrlemoffres  7884  suplocsrlem  7892  rereceu  7973  recriota  7974  axarch  7975  axcaucvglemres  7983  axpre-suploclemres  7985  readdcan  8183  cnegex  8221  addcan  8223  addcan2  8224  negeu  8234  ltadd2  8463  recexre  8622  rimul  8629  ltmul1  8636  mulap0  8698  mulcanapd  8705  suprzclex  9441  zsupcllemex  10337  zssinfcl  10339  suprzubdc  10343  zsupssdc  10345  suprzcl2dc  10346  qbtwnre  10363  hashcl  10890  hashen  10893  fihashdom  10912  hashunlem  10913  hashun  10914  zfz1iso  10950  lencl  10956  sswrd  10961  cvg1nlemres  11167  cvg1n  11168  recvguniq  11177  resqrexlemoverl  11203  resqrexlemex  11207  fimaxre2  11409  climge0  11507  climrecvg1n  11530  fsum3cvg3  11578  expcnvre  11685  mertenslemub  11716  efcllem  11841  oexpneg  12059  bitsfzolem  12136  bitsfi  12139  bezoutlemnewy  12188  bezoutlemstep  12189  dfgcd3  12202  bezout  12203  isprm5lem  12334  ennnfonelemex  12656  ennnfonelemrnh  12658  ennnfonelemf1  12660  ennnfonelemrn  12661  ennnfonelemdm  12662  ennnfonelemnn0  12664  ctinfomlemom  12669  ctinf  12672  ctiunctlemfo  12681  nninfdclemcl  12690  nninfdc  12695  grpinvalem  13087  grprida  13089  grprcan  13239  restbasg  14488  cnpnei  14539  cnptopco  14542  xmettx  14830  metcnpi3  14837  mulcncf  14928  dedekindeulemuub  14937  dedekindeulemub  14938  dedekindeulemlu  14941  dedekindicclemuub  14946  dedekindicclemub  14947  dedekindicclemlu  14950  dedekindicc  14953  ivthinclemlopn  14956  ivthinclemuopn  14958  ivthreinc  14965  ivthdichlem  14971  limcimolemlt  14984  limcimo  14985  limccnp2cntop  14997  reeff1oleme  15092  eflt  15095  bj-charfunr  15540  qdencn  15758  trilpolemlt1  15772  nconstwlpolemgt0  15795