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  4710  tfrlemisucaccv  6482  tfrexlem  6491  tfr1onlemsucaccv  6498  tfrcllemsucaccv  6511  fict  7043  fidceq  7044  dif1enen  7055  php5fin  7057  fisbth  7058  fin0  7060  fin0or  7061  diffisn  7068  infnfi  7070  fidcen  7074  fientri3  7093  unsnfi  7097  unsnfidcex  7098  unsnfidcel  7099  fiuni  7161  ctmlemr  7291  ctssdccl  7294  fodjum  7329  fodju0  7330  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  cc2lem  7468  prarloclemarch2  7622  addlocpr  7739  nqprl  7754  nqpru  7755  appdiv0nq  7767  prmuloc  7769  mullocpr  7774  ltprordil  7792  ltaddpr  7800  ltexprlemopl  7804  ltexprlemopu  7806  ltexprlemloc  7810  ltexprlemrl  7813  ltexprlemru  7815  addcanprleml  7817  addcanprlemu  7818  ltaprlem  7821  ltaprg  7822  prplnqu  7823  recexprlemloc  7834  recexprlem1ssl  7836  recexprlem1ssu  7837  aptiprleml  7842  aptiprlemu  7843  ltmprr  7845  archpr  7846  cauappcvgprlemopl  7849  cauappcvgprlemopu  7851  cauappcvgprlemloc  7855  cauappcvgprlem1  7862  cauappcvgprlem2  7863  archrecpr  7867  caucvgprlemopl  7872  caucvgprlemopu  7874  caucvgprlemloc  7878  caucvgprlem2  7883  caucvgprprlemml  7897  caucvgprprlemmu  7898  caucvgprprlemopl  7900  caucvgprprlemopu  7902  caucvgprprlemloc  7906  caucvgprprlemexbt  7909  caucvgprprlem2  7913  suplocexprlemrl  7920  suplocexprlemmu  7921  suplocexprlemru  7922  suplocexprlemdisj  7923  suplocexprlemloc  7924  suplocexprlemex  7925  suplocexprlemub  7926  suplocexprlemlub  7927  prsrriota  7991  caucvgsrlemgt1  7998  caucvgsrlemoffres  8003  suplocsrlem  8011  rereceu  8092  recriota  8093  axarch  8094  axcaucvglemres  8102  axpre-suploclemres  8104  readdcan  8302  cnegex  8340  addcan  8342  addcan2  8343  negeu  8353  ltadd2  8582  recexre  8741  rimul  8748  ltmul1  8755  mulap0  8817  mulcanapd  8824  suprzclex  9561  zsupcllemex  10467  zssinfcl  10469  suprzubdc  10473  zsupssdc  10475  suprzcl2dc  10476  qbtwnre  10493  hashcl  11020  hashen  11023  fihashdom  11042  hashunlem  11043  hashun  11044  zfz1iso  11081  lencl  11093  sswrd  11098  cvg1nlemres  11517  cvg1n  11518  recvguniq  11527  resqrexlemoverl  11553  resqrexlemex  11557  fimaxre2  11759  climge0  11857  climrecvg1n  11880  fsum3cvg3  11928  expcnvre  12035  mertenslemub  12066  efcllem  12191  oexpneg  12409  bitsfzolem  12486  bitsfi  12489  bezoutlemnewy  12538  bezoutlemstep  12539  dfgcd3  12552  bezout  12553  isprm5lem  12684  ennnfonelemex  13006  ennnfonelemrnh  13008  ennnfonelemf1  13010  ennnfonelemrn  13011  ennnfonelemdm  13012  ennnfonelemnn0  13014  ctinfomlemom  13019  ctinf  13022  ctiunctlemfo  13031  nninfdclemcl  13040  nninfdc  13045  grpinvalem  13439  grprida  13441  grprcan  13591  mplsubgfilemcl  14684  restbasg  14863  cnpnei  14914  cnptopco  14917  xmettx  15205  metcnpi3  15212  mulcncf  15303  dedekindeulemuub  15312  dedekindeulemub  15313  dedekindeulemlu  15316  dedekindicclemuub  15321  dedekindicclemub  15322  dedekindicclemlu  15325  dedekindicc  15328  ivthinclemlopn  15331  ivthinclemuopn  15333  ivthreinc  15340  ivthdichlem  15346  limcimolemlt  15359  limcimo  15360  limccnp2cntop  15372  reeff1oleme  15467  eflt  15470  upgredg  15963  bj-charfunr  16282  qdencn  16509  trilpolemlt1  16523  nconstwlpolemgt0  16546