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  4077  nnsucpred  4708  tfrlemisucaccv  6469  tfrexlem  6478  tfr1onlemsucaccv  6485  tfrcllemsucaccv  6498  fict  7026  fidceq  7027  dif1enen  7038  php5fin  7040  fisbth  7041  fin0  7043  fin0or  7044  diffisn  7051  infnfi  7053  fientri3  7073  unsnfi  7077  unsnfidcex  7078  unsnfidcel  7079  fiuni  7141  ctmlemr  7271  ctssdccl  7274  fodjum  7309  fodju0  7310  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  cc2lem  7448  prarloclemarch2  7602  addlocpr  7719  nqprl  7734  nqpru  7735  appdiv0nq  7747  prmuloc  7749  mullocpr  7754  ltprordil  7772  ltaddpr  7780  ltexprlemopl  7784  ltexprlemopu  7786  ltexprlemloc  7790  ltexprlemrl  7793  ltexprlemru  7795  addcanprleml  7797  addcanprlemu  7798  ltaprlem  7801  ltaprg  7802  prplnqu  7803  recexprlemloc  7814  recexprlem1ssl  7816  recexprlem1ssu  7817  aptiprleml  7822  aptiprlemu  7823  ltmprr  7825  archpr  7826  cauappcvgprlemopl  7829  cauappcvgprlemopu  7831  cauappcvgprlemloc  7835  cauappcvgprlem1  7842  cauappcvgprlem2  7843  archrecpr  7847  caucvgprlemopl  7852  caucvgprlemopu  7854  caucvgprlemloc  7858  caucvgprlem2  7863  caucvgprprlemml  7877  caucvgprprlemmu  7878  caucvgprprlemopl  7880  caucvgprprlemopu  7882  caucvgprprlemloc  7886  caucvgprprlemexbt  7889  caucvgprprlem2  7893  suplocexprlemrl  7900  suplocexprlemmu  7901  suplocexprlemru  7902  suplocexprlemdisj  7903  suplocexprlemloc  7904  suplocexprlemex  7905  suplocexprlemub  7906  suplocexprlemlub  7907  prsrriota  7971  caucvgsrlemgt1  7978  caucvgsrlemoffres  7983  suplocsrlem  7991  rereceu  8072  recriota  8073  axarch  8074  axcaucvglemres  8082  axpre-suploclemres  8084  readdcan  8282  cnegex  8320  addcan  8322  addcan2  8323  negeu  8333  ltadd2  8562  recexre  8721  rimul  8728  ltmul1  8735  mulap0  8797  mulcanapd  8804  suprzclex  9541  zsupcllemex  10445  zssinfcl  10447  suprzubdc  10451  zsupssdc  10453  suprzcl2dc  10454  qbtwnre  10471  hashcl  10998  hashen  11001  fihashdom  11020  hashunlem  11021  hashun  11022  zfz1iso  11058  lencl  11070  sswrd  11075  cvg1nlemres  11491  cvg1n  11492  recvguniq  11501  resqrexlemoverl  11527  resqrexlemex  11531  fimaxre2  11733  climge0  11831  climrecvg1n  11854  fsum3cvg3  11902  expcnvre  12009  mertenslemub  12040  efcllem  12165  oexpneg  12383  bitsfzolem  12460  bitsfi  12463  bezoutlemnewy  12512  bezoutlemstep  12513  dfgcd3  12526  bezout  12527  isprm5lem  12658  ennnfonelemex  12980  ennnfonelemrnh  12982  ennnfonelemf1  12984  ennnfonelemrn  12985  ennnfonelemdm  12986  ennnfonelemnn0  12988  ctinfomlemom  12993  ctinf  12996  ctiunctlemfo  13005  nninfdclemcl  13014  nninfdc  13019  grpinvalem  13413  grprida  13415  grprcan  13565  mplsubgfilemcl  14657  restbasg  14836  cnpnei  14887  cnptopco  14890  xmettx  15178  metcnpi3  15185  mulcncf  15276  dedekindeulemuub  15285  dedekindeulemub  15286  dedekindeulemlu  15289  dedekindicclemuub  15294  dedekindicclemub  15295  dedekindicclemlu  15298  dedekindicc  15301  ivthinclemlopn  15304  ivthinclemuopn  15306  ivthreinc  15313  ivthdichlem  15319  limcimolemlt  15332  limcimo  15333  limccnp2cntop  15345  reeff1oleme  15440  eflt  15443  upgredg  15936  bj-charfunr  16131  qdencn  16354  trilpolemlt1  16368  nconstwlpolemgt0  16391