Theorem rexlimddv 2673

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∃wrex 2529

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is referenced by:  disjiun  4120  nnsucpred  4759  tfrlemisucaccv  6586  tfrexlem  6595  tfr1onlemsucaccv  6602  tfrcllemsucaccv  6615  fict  7160  fidceq  7161  dif1enen  7174  php5fin  7176  fisbth  7177  fin0  7179  fin0or  7180  diffisn  7187  infnfi  7189  fidcen  7193  fientri3  7212  unsnfi  7216  unsnfidcex  7217  unsnfidcel  7218  fiuni  7302  ctmlemr  7438  ctssdccl  7441  fodjum  7476  fodju0  7477  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  cc2lem  7622  prarloclemarch2  7776  addlocpr  7893  nqprl  7908  nqpru  7909  appdiv0nq  7921  prmuloc  7923  mullocpr  7928  ltprordil  7946  ltaddpr  7954  ltexprlemopl  7958  ltexprlemopu  7960  ltexprlemloc  7964  ltexprlemrl  7967  ltexprlemru  7969  addcanprleml  7971  addcanprlemu  7972  ltaprlem  7975  ltaprg  7976  prplnqu  7977  recexprlemloc  7988  recexprlem1ssl  7990  recexprlem1ssu  7991  aptiprleml  7996  aptiprlemu  7997  ltmprr  7999  archpr  8000  cauappcvgprlemopl  8003  cauappcvgprlemopu  8005  cauappcvgprlemloc  8009  cauappcvgprlem1  8016  cauappcvgprlem2  8017  archrecpr  8021  caucvgprlemopl  8026  caucvgprlemopu  8028  caucvgprlemloc  8032  caucvgprlem2  8037  caucvgprprlemml  8051  caucvgprprlemmu  8052  caucvgprprlemopl  8054  caucvgprprlemopu  8056  caucvgprprlemloc  8060  caucvgprprlemexbt  8063  caucvgprprlem2  8067  suplocexprlemrl  8074  suplocexprlemmu  8075  suplocexprlemru  8076  suplocexprlemdisj  8077  suplocexprlemloc  8078  suplocexprlemex  8079  suplocexprlemub  8080  suplocexprlemlub  8081  prsrriota  8145  caucvgsrlemgt1  8152  caucvgsrlemoffres  8157  suplocsrlem  8165  rereceu  8246  recriota  8247  axarch  8248  axcaucvglemres  8256  axpre-suploclemres  8258  readdcan  8456  cnegex  8494  addcan  8496  addcan2  8497  negeu  8507  ltadd2  8737  recexre  8896  rimul  8903  ltmul1  8910  mulap0  8972  mulcanapd  8979  suprzclex  9723  zsupcllemex  10641  zssinfcl  10643  suprzubdc  10649  zsupssdc  10651  suprzcl2dc  10652  qbtwnre  10669  hashcl  11198  hashen  11201  fihashdom  11221  hashunlem  11222  hashun  11223  zfz1iso  11271  lencl  11286  sswrd  11291  cvg1nlemres  11729  cvg1n  11730  recvguniq  11739  resqrexlemoverl  11765  resqrexlemex  11769  fimaxre2  11971  climge0  12069  climrecvg1n  12092  fsum3cvg3  12141  expcnvre  12248  mertenslemub  12279  efcllem  12404  oexpneg  12622  bitsfzolem  12699  bitsfi  12702  bezoutlemnewy  12751  bezoutlemstep  12752  dfgcd3  12765  bezout  12766  isprm5lem  12897  ballotfilemscl  13225  ballotfilemsle  13226  ennnfonelemex  13283  ennnfonelemrnh  13285  ennnfonelemf1  13287  ennnfonelemrn  13288  ennnfonelemdm  13289  ennnfonelemnn0  13291  ctinfomlemom  13296  ctinf  13299  ctiunctlemfo  13308  nninfdclemcl  13317  nninfdc  13322  grpinvalem  13682  grprida  13684  grprcan  13819  mplsubgfilemcl  15013  restbasg  15192  cnpnei  15243  cnptopco  15246  xmettx  15534  metcnpi3  15541  mulcncf  15632  dedekindeulemuub  15641  dedekindeulemub  15642  dedekindeulemlu  15645  dedekindicclemuub  15650  dedekindicclemub  15651  dedekindicclemlu  15654  dedekindicc  15657  ivthinclemlopn  15660  ivthinclemuopn  15662  ivthreinc  15669  ivthdichlem  15675  limcimolemlt  15688  limcimo  15689  limccnp2cntop  15701  reeff1oleme  15796  eflt  15799  upgredg  16299  bj-charfunr  16750  qdencn  16977  trilpolemlt1  16995  nconstwlpolemgt0  17019