Theorem rexlimddv 2592

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2141  ∃wrex 2449

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453  df-rex 2454

This theorem is referenced by:  disjiun  3982  nnsucpred  4599  tfrlemisucaccv  6301  tfrexlem  6310  tfr1onlemsucaccv  6317  tfrcllemsucaccv  6330  fict  6842  fidceq  6843  dif1enen  6854  php5fin  6856  fisbth  6857  fin0  6859  fin0or  6860  diffisn  6867  infnfi  6869  fientri3  6888  unsnfi  6892  unsnfidcex  6893  unsnfidcel  6894  fiuni  6951  ctmlemr  7081  ctssdccl  7084  fodjum  7118  fodju0  7119  exmidfodomrlemr  7166  exmidfodomrlemrALT  7167  cc2lem  7215  prarloclemarch2  7368  addlocpr  7485  nqprl  7500  nqpru  7501  appdiv0nq  7513  prmuloc  7515  mullocpr  7520  ltprordil  7538  ltaddpr  7546  ltexprlemopl  7550  ltexprlemopu  7552  ltexprlemloc  7556  ltexprlemrl  7559  ltexprlemru  7561  addcanprleml  7563  addcanprlemu  7564  ltaprlem  7567  ltaprg  7568  prplnqu  7569  recexprlemloc  7580  recexprlem1ssl  7582  recexprlem1ssu  7583  aptiprleml  7588  aptiprlemu  7589  ltmprr  7591  archpr  7592  cauappcvgprlemopl  7595  cauappcvgprlemopu  7597  cauappcvgprlemloc  7601  cauappcvgprlem1  7608  cauappcvgprlem2  7609  archrecpr  7613  caucvgprlemopl  7618  caucvgprlemopu  7620  caucvgprlemloc  7624  caucvgprlem2  7629  caucvgprprlemml  7643  caucvgprprlemmu  7644  caucvgprprlemopl  7646  caucvgprprlemopu  7648  caucvgprprlemloc  7652  caucvgprprlemexbt  7655  caucvgprprlem2  7659  suplocexprlemrl  7666  suplocexprlemmu  7667  suplocexprlemru  7668  suplocexprlemdisj  7669  suplocexprlemloc  7670  suplocexprlemex  7671  suplocexprlemub  7672  suplocexprlemlub  7673  prsrriota  7737  caucvgsrlemgt1  7744  caucvgsrlemoffres  7749  suplocsrlem  7757  rereceu  7838  recriota  7839  axarch  7840  axcaucvglemres  7848  axpre-suploclemres  7850  readdcan  8046  cnegex  8084  addcan  8086  addcan2  8087  negeu  8097  ltadd2  8325  recexre  8484  rimul  8491  ltmul1  8498  mulap0  8559  mulcanapd  8566  suprzclex  9297  qbtwnre  10200  hashcl  10702  hashen  10705  fihashdom  10725  hashunlem  10726  hashun  10727  zfz1iso  10763  cvg1nlemres  10936  cvg1n  10937  recvguniq  10946  resqrexlemoverl  10972  resqrexlemex  10976  fimaxre2  11177  climge0  11275  climrecvg1n  11298  fsum3cvg3  11346  expcnvre  11453  mertenslemub  11484  efcllem  11609  oexpneg  11823  zsupcllemex  11888  zssinfcl  11890  suprzubdc  11894  zsupssdc  11896  suprzcl2dc  11897  bezoutlemnewy  11938  bezoutlemstep  11939  dfgcd3  11952  bezout  11953  isprm5lem  12082  ennnfonelemex  12356  ennnfonelemrnh  12358  ennnfonelemf1  12360  ennnfonelemrn  12361  ennnfonelemdm  12362  ennnfonelemnn0  12364  ctinfomlemom  12369  ctinf  12372  ctiunctlemfo  12381  nninfdclemcl  12390  nninfdc  12395  grprinvlem  12626  grpridd  12628  grprcan  12727  restbasg  12921  cnpnei  12972  cnptopco  12975  xmettx  13263  metcnpi3  13270  mulcncf  13344  dedekindeulemuub  13348  dedekindeulemub  13349  dedekindeulemlu  13352  dedekindicclemuub  13357  dedekindicclemub  13358  dedekindicclemlu  13361  dedekindicc  13364  ivthinclemlopn  13367  ivthinclemuopn  13369  limcimolemlt  13386  limcimo  13387  limccnp2cntop  13399  reeff1oleme  13446  eflt  13449  bj-charfunr  13805  qdencn  14019  trilpolemlt1  14033  nconstwlpolemgt0  14055