Theorem rexlimddv 2665

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2203  ∃wrex 2521

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2525  df-rex 2526

This theorem is referenced by:  disjiun  4104  nnsucpred  4739  tfrlemisucaccv  6556  tfrexlem  6565  tfr1onlemsucaccv  6572  tfrcllemsucaccv  6585  fict  7123  fidceq  7124  dif1enen  7137  php5fin  7139  fisbth  7140  fin0  7142  fin0or  7143  diffisn  7150  infnfi  7152  fidcen  7156  fientri3  7175  unsnfi  7179  unsnfidcex  7180  unsnfidcel  7181  fiuni  7265  ctmlemr  7399  ctssdccl  7402  fodjum  7437  fodju0  7438  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  cc2lem  7580  prarloclemarch2  7734  addlocpr  7851  nqprl  7866  nqpru  7867  appdiv0nq  7879  prmuloc  7881  mullocpr  7886  ltprordil  7904  ltaddpr  7912  ltexprlemopl  7916  ltexprlemopu  7918  ltexprlemloc  7922  ltexprlemrl  7925  ltexprlemru  7927  addcanprleml  7929  addcanprlemu  7930  ltaprlem  7933  ltaprg  7934  prplnqu  7935  recexprlemloc  7946  recexprlem1ssl  7948  recexprlem1ssu  7949  aptiprleml  7954  aptiprlemu  7955  ltmprr  7957  archpr  7958  cauappcvgprlemopl  7961  cauappcvgprlemopu  7963  cauappcvgprlemloc  7967  cauappcvgprlem1  7974  cauappcvgprlem2  7975  archrecpr  7979  caucvgprlemopl  7984  caucvgprlemopu  7986  caucvgprlemloc  7990  caucvgprlem2  7995  caucvgprprlemml  8009  caucvgprprlemmu  8010  caucvgprprlemopl  8012  caucvgprprlemopu  8014  caucvgprprlemloc  8018  caucvgprprlemexbt  8021  caucvgprprlem2  8025  suplocexprlemrl  8032  suplocexprlemmu  8033  suplocexprlemru  8034  suplocexprlemdisj  8035  suplocexprlemloc  8036  suplocexprlemex  8037  suplocexprlemub  8038  suplocexprlemlub  8039  prsrriota  8103  caucvgsrlemgt1  8110  caucvgsrlemoffres  8115  suplocsrlem  8123  rereceu  8204  recriota  8205  axarch  8206  axcaucvglemres  8214  axpre-suploclemres  8216  readdcan  8413  cnegex  8451  addcan  8453  addcan2  8454  negeu  8464  ltadd2  8693  recexre  8852  rimul  8859  ltmul1  8866  mulap0  8928  mulcanapd  8935  suprzclex  9676  zsupcllemex  10590  zssinfcl  10592  suprzubdc  10596  zsupssdc  10598  suprzcl2dc  10599  qbtwnre  10616  hashcl  11144  hashen  11147  fihashdom  11167  hashunlem  11168  hashun  11169  zfz1iso  11213  lencl  11228  sswrd  11233  cvg1nlemres  11670  cvg1n  11671  recvguniq  11680  resqrexlemoverl  11706  resqrexlemex  11710  fimaxre2  11912  climge0  12010  climrecvg1n  12033  fsum3cvg3  12082  expcnvre  12189  mertenslemub  12220  efcllem  12345  oexpneg  12563  bitsfzolem  12640  bitsfi  12643  bezoutlemnewy  12692  bezoutlemstep  12693  dfgcd3  12706  bezout  12707  isprm5lem  12838  ennnfonelemex  13165  ennnfonelemrnh  13167  ennnfonelemf1  13169  ennnfonelemrn  13170  ennnfonelemdm  13171  ennnfonelemnn0  13173  ctinfomlemom  13178  ctinf  13181  ctiunctlemfo  13190  nninfdclemcl  13199  nninfdc  13204  grpinvalem  13598  grprida  13600  grprcan  13750  mplsubgfilemcl  14854  restbasg  15033  cnpnei  15084  cnptopco  15087  xmettx  15375  metcnpi3  15382  mulcncf  15473  dedekindeulemuub  15482  dedekindeulemub  15483  dedekindeulemlu  15486  dedekindicclemuub  15491  dedekindicclemub  15492  dedekindicclemlu  15495  dedekindicc  15498  ivthinclemlopn  15501  ivthinclemuopn  15503  ivthreinc  15510  ivthdichlem  15516  limcimolemlt  15529  limcimo  15530  limccnp2cntop  15542  reeff1oleme  15637  eflt  15640  upgredg  16139  bj-charfunr  16580  qdencn  16807  trilpolemlt1  16825  nconstwlpolemgt0  16850