Theorem rexlimddv 2587

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2136  ∃wrex 2444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-i5r 1523

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2448  df-rex 2449

This theorem is referenced by:  disjiun  3976  nnsucpred  4593  grprinvlem  6032  grpridd  6034  tfrlemisucaccv  6289  tfrexlem  6298  tfr1onlemsucaccv  6305  tfrcllemsucaccv  6318  fict  6830  fidceq  6831  dif1enen  6842  php5fin  6844  fisbth  6845  fin0  6847  fin0or  6848  diffisn  6855  infnfi  6857  fientri3  6876  unsnfi  6880  unsnfidcex  6881  unsnfidcel  6882  fiuni  6939  ctmlemr  7069  ctssdccl  7072  fodjum  7106  fodju0  7107  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  cc2lem  7203  prarloclemarch2  7356  addlocpr  7473  nqprl  7488  nqpru  7489  appdiv0nq  7501  prmuloc  7503  mullocpr  7508  ltprordil  7526  ltaddpr  7534  ltexprlemopl  7538  ltexprlemopu  7540  ltexprlemloc  7544  ltexprlemrl  7547  ltexprlemru  7549  addcanprleml  7551  addcanprlemu  7552  ltaprlem  7555  ltaprg  7556  prplnqu  7557  recexprlemloc  7568  recexprlem1ssl  7570  recexprlem1ssu  7571  aptiprleml  7576  aptiprlemu  7577  ltmprr  7579  archpr  7580  cauappcvgprlemopl  7583  cauappcvgprlemopu  7585  cauappcvgprlemloc  7589  cauappcvgprlem1  7596  cauappcvgprlem2  7597  archrecpr  7601  caucvgprlemopl  7606  caucvgprlemopu  7608  caucvgprlemloc  7612  caucvgprlem2  7617  caucvgprprlemml  7631  caucvgprprlemmu  7632  caucvgprprlemopl  7634  caucvgprprlemopu  7636  caucvgprprlemloc  7640  caucvgprprlemexbt  7643  caucvgprprlem2  7647  suplocexprlemrl  7654  suplocexprlemmu  7655  suplocexprlemru  7656  suplocexprlemdisj  7657  suplocexprlemloc  7658  suplocexprlemex  7659  suplocexprlemub  7660  suplocexprlemlub  7661  prsrriota  7725  caucvgsrlemgt1  7732  caucvgsrlemoffres  7737  suplocsrlem  7745  rereceu  7826  recriota  7827  axarch  7828  axcaucvglemres  7836  axpre-suploclemres  7838  readdcan  8034  cnegex  8072  addcan  8074  addcan2  8075  negeu  8085  ltadd2  8313  recexre  8472  rimul  8479  ltmul1  8486  mulap0  8547  mulcanapd  8554  suprzclex  9285  qbtwnre  10188  hashcl  10690  hashen  10693  fihashdom  10712  hashunlem  10713  hashun  10714  zfz1iso  10750  cvg1nlemres  10923  cvg1n  10924  recvguniq  10933  resqrexlemoverl  10959  resqrexlemex  10963  fimaxre2  11164  climge0  11262  climrecvg1n  11285  fsum3cvg3  11333  expcnvre  11440  mertenslemub  11471  efcllem  11596  oexpneg  11810  zsupcllemex  11875  zssinfcl  11877  suprzubdc  11881  zsupssdc  11883  suprzcl2dc  11884  bezoutlemnewy  11925  bezoutlemstep  11926  dfgcd3  11939  bezout  11940  isprm5lem  12069  ennnfonelemex  12343  ennnfonelemrnh  12345  ennnfonelemf1  12347  ennnfonelemrn  12348  ennnfonelemdm  12349  ennnfonelemnn0  12351  ctinfomlemom  12356  ctinf  12359  ctiunctlemfo  12368  nninfdclemcl  12377  nninfdc  12382  restbasg  12768  cnpnei  12819  cnptopco  12822  xmettx  13110  metcnpi3  13117  mulcncf  13191  dedekindeulemuub  13195  dedekindeulemub  13196  dedekindeulemlu  13199  dedekindicclemuub  13204  dedekindicclemub  13205  dedekindicclemlu  13208  dedekindicc  13211  ivthinclemlopn  13214  ivthinclemuopn  13216  limcimolemlt  13233  limcimo  13234  limccnp2cntop  13246  reeff1oleme  13293  eflt  13296  bj-charfunr  13652  qdencn  13866  trilpolemlt1  13880  nconstwlpolemgt0  13902