Theorem rexlimddv 2599

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  ∃wrex 2456

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  disjiun  3999  nnsucpred  4617  tfrlemisucaccv  6326  tfrexlem  6335  tfr1onlemsucaccv  6342  tfrcllemsucaccv  6355  fict  6868  fidceq  6869  dif1enen  6880  php5fin  6882  fisbth  6883  fin0  6885  fin0or  6886  diffisn  6893  infnfi  6895  fientri3  6914  unsnfi  6918  unsnfidcex  6919  unsnfidcel  6920  fiuni  6977  ctmlemr  7107  ctssdccl  7110  fodjum  7144  fodju0  7145  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  cc2lem  7265  prarloclemarch2  7418  addlocpr  7535  nqprl  7550  nqpru  7551  appdiv0nq  7563  prmuloc  7565  mullocpr  7570  ltprordil  7588  ltaddpr  7596  ltexprlemopl  7600  ltexprlemopu  7602  ltexprlemloc  7606  ltexprlemrl  7609  ltexprlemru  7611  addcanprleml  7613  addcanprlemu  7614  ltaprlem  7617  ltaprg  7618  prplnqu  7619  recexprlemloc  7630  recexprlem1ssl  7632  recexprlem1ssu  7633  aptiprleml  7638  aptiprlemu  7639  ltmprr  7641  archpr  7642  cauappcvgprlemopl  7645  cauappcvgprlemopu  7647  cauappcvgprlemloc  7651  cauappcvgprlem1  7658  cauappcvgprlem2  7659  archrecpr  7663  caucvgprlemopl  7668  caucvgprlemopu  7670  caucvgprlemloc  7674  caucvgprlem2  7679  caucvgprprlemml  7693  caucvgprprlemmu  7694  caucvgprprlemopl  7696  caucvgprprlemopu  7698  caucvgprprlemloc  7702  caucvgprprlemexbt  7705  caucvgprprlem2  7709  suplocexprlemrl  7716  suplocexprlemmu  7717  suplocexprlemru  7718  suplocexprlemdisj  7719  suplocexprlemloc  7720  suplocexprlemex  7721  suplocexprlemub  7722  suplocexprlemlub  7723  prsrriota  7787  caucvgsrlemgt1  7794  caucvgsrlemoffres  7799  suplocsrlem  7807  rereceu  7888  recriota  7889  axarch  7890  axcaucvglemres  7898  axpre-suploclemres  7900  readdcan  8097  cnegex  8135  addcan  8137  addcan2  8138  negeu  8148  ltadd2  8376  recexre  8535  rimul  8542  ltmul1  8549  mulap0  8611  mulcanapd  8618  suprzclex  9351  qbtwnre  10257  hashcl  10761  hashen  10764  fihashdom  10783  hashunlem  10784  hashun  10785  zfz1iso  10821  cvg1nlemres  10994  cvg1n  10995  recvguniq  11004  resqrexlemoverl  11030  resqrexlemex  11034  fimaxre2  11235  climge0  11333  climrecvg1n  11356  fsum3cvg3  11404  expcnvre  11511  mertenslemub  11542  efcllem  11667  oexpneg  11882  zsupcllemex  11947  zssinfcl  11949  suprzubdc  11953  zsupssdc  11955  suprzcl2dc  11956  bezoutlemnewy  11997  bezoutlemstep  11998  dfgcd3  12011  bezout  12012  isprm5lem  12141  ennnfonelemex  12415  ennnfonelemrnh  12417  ennnfonelemf1  12419  ennnfonelemrn  12420  ennnfonelemdm  12421  ennnfonelemnn0  12423  ctinfomlemom  12428  ctinf  12431  ctiunctlemfo  12440  nninfdclemcl  12449  nninfdc  12454  grprinvlem  12804  grpridd  12806  grprcan  12910  restbasg  13671  cnpnei  13722  cnptopco  13725  xmettx  14013  metcnpi3  14020  mulcncf  14094  dedekindeulemuub  14098  dedekindeulemub  14099  dedekindeulemlu  14102  dedekindicclemuub  14107  dedekindicclemub  14108  dedekindicclemlu  14111  dedekindicc  14114  ivthinclemlopn  14117  ivthinclemuopn  14119  limcimolemlt  14136  limcimo  14137  limccnp2cntop  14149  reeff1oleme  14196  eflt  14199  bj-charfunr  14565  qdencn  14778  trilpolemlt1  14792  nconstwlpolemgt0  14814