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  6491  tfrexlem  6500  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  fict  7055  fidceq  7056  dif1enen  7069  php5fin  7071  fisbth  7072  fin0  7074  fin0or  7075  diffisn  7082  infnfi  7084  fidcen  7088  fientri3  7107  unsnfi  7111  unsnfidcex  7112  unsnfidcel  7113  fiuni  7177  ctmlemr  7307  ctssdccl  7310  fodjum  7345  fodju0  7346  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  cc2lem  7485  prarloclemarch2  7639  addlocpr  7756  nqprl  7771  nqpru  7772  appdiv0nq  7784  prmuloc  7786  mullocpr  7791  ltprordil  7809  ltaddpr  7817  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemloc  7827  ltexprlemrl  7830  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  ltaprlem  7838  ltaprg  7839  prplnqu  7840  recexprlemloc  7851  recexprlem1ssl  7853  recexprlem1ssu  7854  aptiprleml  7859  aptiprlemu  7860  ltmprr  7862  archpr  7863  cauappcvgprlemopl  7866  cauappcvgprlemopu  7868  cauappcvgprlemloc  7872  cauappcvgprlem1  7879  cauappcvgprlem2  7880  archrecpr  7884  caucvgprlemopl  7889  caucvgprlemopu  7891  caucvgprlemloc  7895  caucvgprlem2  7900  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemopu  7919  caucvgprprlemloc  7923  caucvgprprlemexbt  7926  caucvgprprlem2  7930  suplocexprlemrl  7937  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemex  7942  suplocexprlemub  7943  suplocexprlemlub  7944  prsrriota  8008  caucvgsrlemgt1  8015  caucvgsrlemoffres  8020  suplocsrlem  8028  rereceu  8109  recriota  8110  axarch  8111  axcaucvglemres  8119  axpre-suploclemres  8121  readdcan  8319  cnegex  8357  addcan  8359  addcan2  8360  negeu  8370  ltadd2  8599  recexre  8758  rimul  8765  ltmul1  8772  mulap0  8834  mulcanapd  8841  suprzclex  9578  zsupcllemex  10491  zssinfcl  10493  suprzubdc  10497  zsupssdc  10499  suprzcl2dc  10500  qbtwnre  10517  hashcl  11044  hashen  11047  fihashdom  11067  hashunlem  11068  hashun  11069  zfz1iso  11106  lencl  11121  sswrd  11126  cvg1nlemres  11550  cvg1n  11551  recvguniq  11560  resqrexlemoverl  11586  resqrexlemex  11590  fimaxre2  11792  climge0  11890  climrecvg1n  11913  fsum3cvg3  11962  expcnvre  12069  mertenslemub  12100  efcllem  12225  oexpneg  12443  bitsfzolem  12520  bitsfi  12523  bezoutlemnewy  12572  bezoutlemstep  12573  dfgcd3  12586  bezout  12587  isprm5lem  12718  ennnfonelemex  13040  ennnfonelemrnh  13042  ennnfonelemf1  13044  ennnfonelemrn  13045  ennnfonelemdm  13046  ennnfonelemnn0  13048  ctinfomlemom  13053  ctinf  13056  ctiunctlemfo  13065  nninfdclemcl  13074  nninfdc  13079  grpinvalem  13473  grprida  13475  grprcan  13625  mplsubgfilemcl  14719  restbasg  14898  cnpnei  14949  cnptopco  14952  xmettx  15240  metcnpi3  15247  mulcncf  15338  dedekindeulemuub  15347  dedekindeulemub  15348  dedekindeulemlu  15351  dedekindicclemuub  15356  dedekindicclemub  15357  dedekindicclemlu  15360  dedekindicc  15363  ivthinclemlopn  15366  ivthinclemuopn  15368  ivthreinc  15375  ivthdichlem  15381  limcimolemlt  15394  limcimo  15395  limccnp2cntop  15407  reeff1oleme  15502  eflt  15505  upgredg  16001  bj-charfunr  16431  qdencn  16657  trilpolemlt1  16671  nconstwlpolemgt0  16695