Theorem rexlimddv 2655

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  ∃wrex 2511

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515  df-rex 2516

This theorem is referenced by:  disjiun  4083  nnsucpred  4715  tfrlemisucaccv  6490  tfrexlem  6499  tfr1onlemsucaccv  6506  tfrcllemsucaccv  6519  fict  7054  fidceq  7055  dif1enen  7068  php5fin  7070  fisbth  7071  fin0  7073  fin0or  7074  diffisn  7081  infnfi  7083  fidcen  7087  fientri3  7106  unsnfi  7110  unsnfidcex  7111  unsnfidcel  7112  fiuni  7176  ctmlemr  7306  ctssdccl  7309  fodjum  7344  fodju0  7345  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  cc2lem  7484  prarloclemarch2  7638  addlocpr  7755  nqprl  7770  nqpru  7771  appdiv0nq  7783  prmuloc  7785  mullocpr  7790  ltprordil  7808  ltaddpr  7816  ltexprlemopl  7820  ltexprlemopu  7822  ltexprlemloc  7826  ltexprlemrl  7829  ltexprlemru  7831  addcanprleml  7833  addcanprlemu  7834  ltaprlem  7837  ltaprg  7838  prplnqu  7839  recexprlemloc  7850  recexprlem1ssl  7852  recexprlem1ssu  7853  aptiprleml  7858  aptiprlemu  7859  ltmprr  7861  archpr  7862  cauappcvgprlemopl  7865  cauappcvgprlemopu  7867  cauappcvgprlemloc  7871  cauappcvgprlem1  7878  cauappcvgprlem2  7879  archrecpr  7883  caucvgprlemopl  7888  caucvgprlemopu  7890  caucvgprlemloc  7894  caucvgprlem2  7899  caucvgprprlemml  7913  caucvgprprlemmu  7914  caucvgprprlemopl  7916  caucvgprprlemopu  7918  caucvgprprlemloc  7922  caucvgprprlemexbt  7925  caucvgprprlem2  7929  suplocexprlemrl  7936  suplocexprlemmu  7937  suplocexprlemru  7938  suplocexprlemdisj  7939  suplocexprlemloc  7940  suplocexprlemex  7941  suplocexprlemub  7942  suplocexprlemlub  7943  prsrriota  8007  caucvgsrlemgt1  8014  caucvgsrlemoffres  8019  suplocsrlem  8027  rereceu  8108  recriota  8109  axarch  8110  axcaucvglemres  8118  axpre-suploclemres  8120  readdcan  8318  cnegex  8356  addcan  8358  addcan2  8359  negeu  8369  ltadd2  8598  recexre  8757  rimul  8764  ltmul1  8771  mulap0  8833  mulcanapd  8840  suprzclex  9577  zsupcllemex  10489  zssinfcl  10491  suprzubdc  10495  zsupssdc  10497  suprzcl2dc  10498  qbtwnre  10515  hashcl  11042  hashen  11045  fihashdom  11065  hashunlem  11066  hashun  11067  zfz1iso  11104  lencl  11116  sswrd  11121  cvg1nlemres  11545  cvg1n  11546  recvguniq  11555  resqrexlemoverl  11581  resqrexlemex  11585  fimaxre2  11787  climge0  11885  climrecvg1n  11908  fsum3cvg3  11956  expcnvre  12063  mertenslemub  12094  efcllem  12219  oexpneg  12437  bitsfzolem  12514  bitsfi  12517  bezoutlemnewy  12566  bezoutlemstep  12567  dfgcd3  12580  bezout  12581  isprm5lem  12712  ennnfonelemex  13034  ennnfonelemrnh  13036  ennnfonelemf1  13038  ennnfonelemrn  13039  ennnfonelemdm  13040  ennnfonelemnn0  13042  ctinfomlemom  13047  ctinf  13050  ctiunctlemfo  13059  nninfdclemcl  13068  nninfdc  13073  grpinvalem  13467  grprida  13469  grprcan  13619  mplsubgfilemcl  14712  restbasg  14891  cnpnei  14942  cnptopco  14945  xmettx  15233  metcnpi3  15240  mulcncf  15331  dedekindeulemuub  15340  dedekindeulemub  15341  dedekindeulemlu  15344  dedekindicclemuub  15349  dedekindicclemub  15350  dedekindicclemlu  15353  dedekindicc  15356  ivthinclemlopn  15359  ivthinclemuopn  15361  ivthreinc  15368  ivthdichlem  15374  limcimolemlt  15387  limcimo  15388  limccnp2cntop  15400  reeff1oleme  15495  eflt  15498  upgredg  15994  bj-charfunr  16405  qdencn  16631  trilpolemlt1  16645  nconstwlpolemgt0  16668