Theorem rexlimddv 2667

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  ∃wrex 2523

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 2527  df-rex 2528

This theorem is referenced by:  disjiun  4109  nnsucpred  4744  tfrlemisucaccv  6569  tfrexlem  6578  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  fict  7136  fidceq  7137  dif1enen  7150  php5fin  7152  fisbth  7153  fin0  7155  fin0or  7156  diffisn  7163  infnfi  7165  fidcen  7169  fientri3  7188  unsnfi  7192  unsnfidcex  7193  unsnfidcel  7194  fiuni  7278  ctmlemr  7412  ctssdccl  7415  fodjum  7450  fodju0  7451  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  cc2lem  7596  prarloclemarch2  7750  addlocpr  7867  nqprl  7882  nqpru  7883  appdiv0nq  7895  prmuloc  7897  mullocpr  7902  ltprordil  7920  ltaddpr  7928  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemloc  7938  ltexprlemrl  7941  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  ltaprlem  7949  ltaprg  7950  prplnqu  7951  recexprlemloc  7962  recexprlem1ssl  7964  recexprlem1ssu  7965  aptiprleml  7970  aptiprlemu  7971  ltmprr  7973  archpr  7974  cauappcvgprlemopl  7977  cauappcvgprlemopu  7979  cauappcvgprlemloc  7983  cauappcvgprlem1  7990  cauappcvgprlem2  7991  archrecpr  7995  caucvgprlemopl  8000  caucvgprlemopu  8002  caucvgprlemloc  8006  caucvgprlem2  8011  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemopl  8028  caucvgprprlemopu  8030  caucvgprprlemloc  8034  caucvgprprlemexbt  8037  caucvgprprlem2  8041  suplocexprlemrl  8048  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemex  8053  suplocexprlemub  8054  suplocexprlemlub  8055  prsrriota  8119  caucvgsrlemgt1  8126  caucvgsrlemoffres  8131  suplocsrlem  8139  rereceu  8220  recriota  8221  axarch  8222  axcaucvglemres  8230  axpre-suploclemres  8232  readdcan  8429  cnegex  8467  addcan  8469  addcan2  8470  negeu  8480  ltadd2  8710  recexre  8869  rimul  8876  ltmul1  8883  mulap0  8945  mulcanapd  8952  suprzclex  9694  zsupcllemex  10612  zssinfcl  10614  suprzubdc  10620  zsupssdc  10622  suprzcl2dc  10623  qbtwnre  10640  hashcl  11169  hashen  11172  fihashdom  11192  hashunlem  11193  hashun  11194  zfz1iso  11238  lencl  11253  sswrd  11258  cvg1nlemres  11695  cvg1n  11696  recvguniq  11705  resqrexlemoverl  11731  resqrexlemex  11735  fimaxre2  11937  climge0  12035  climrecvg1n  12058  fsum3cvg3  12107  expcnvre  12214  mertenslemub  12245  efcllem  12370  oexpneg  12588  bitsfzolem  12665  bitsfi  12668  bezoutlemnewy  12717  bezoutlemstep  12718  dfgcd3  12731  bezout  12732  isprm5lem  12863  ballotfilemscl  13191  ballotfilemsle  13192  ennnfonelemex  13249  ennnfonelemrnh  13251  ennnfonelemf1  13253  ennnfonelemrn  13254  ennnfonelemdm  13255  ennnfonelemnn0  13257  ctinfomlemom  13262  ctinf  13265  ctiunctlemfo  13274  nninfdclemcl  13283  nninfdc  13288  grpinvalem  13648  grprida  13650  grprcan  13792  mplsubgfilemcl  14980  restbasg  15159  cnpnei  15210  cnptopco  15213  xmettx  15501  metcnpi3  15508  mulcncf  15599  dedekindeulemuub  15608  dedekindeulemub  15609  dedekindeulemlu  15612  dedekindicclemuub  15617  dedekindicclemub  15618  dedekindicclemlu  15621  dedekindicc  15624  ivthinclemlopn  15627  ivthinclemuopn  15629  ivthreinc  15636  ivthdichlem  15642  limcimolemlt  15655  limcimo  15656  limccnp2cntop  15668  reeff1oleme  15763  eflt  15766  upgredg  16265  bj-charfunr  16706  qdencn  16933  trilpolemlt1  16951  nconstwlpolemgt0  16976