Theorem rexlimddv 2481

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

Syntax hints:   → wi 4   ∧ wa 102   ∈ wcel 1433  ∃wrex 2349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-i5r 1468

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-ral 2353  df-rex 2354

This theorem is referenced by:  grprinvlem  5715  grpridd  5717  tfrlemisucaccv  5962  tfrexlem  5971  fidceq  6354  php5fin  6366  fisbth  6367  fin0  6369  fin0or  6370  diffisn  6377  fientri3  6381  unsnfi  6384  unsnfidcex  6385  unsnfidcel  6386  prarloclemarch2  6609  addlocpr  6726  nqprl  6741  nqpru  6742  appdiv0nq  6754  prmuloc  6756  mullocpr  6761  ltprordil  6779  ltaddpr  6787  ltexprlemopl  6791  ltexprlemopu  6793  ltexprlemloc  6797  ltexprlemrl  6800  ltexprlemru  6802  addcanprleml  6804  addcanprlemu  6805  ltaprlem  6808  ltaprg  6809  prplnqu  6810  recexprlemloc  6821  recexprlem1ssl  6823  recexprlem1ssu  6824  aptiprleml  6829  aptiprlemu  6830  ltmprr  6832  archpr  6833  cauappcvgprlemopl  6836  cauappcvgprlemopu  6838  cauappcvgprlemloc  6842  cauappcvgprlem1  6849  cauappcvgprlem2  6850  archrecpr  6854  caucvgprlemopl  6859  caucvgprlemopu  6861  caucvgprlemloc  6865  caucvgprlem2  6870  caucvgprprlemml  6884  caucvgprprlemmu  6885  caucvgprprlemopl  6887  caucvgprprlemopu  6889  caucvgprprlemloc  6893  caucvgprprlemexbt  6896  caucvgprprlem2  6900  prsrriota  6964  caucvgsrlemgt1  6971  caucvgsrlemoffres  6976  rereceu  7055  recriota  7056  axarch  7057  axcaucvglemres  7065  readdcan  7248  cnegex  7286  addcan  7288  addcan2  7289  negeu  7299  ltadd2  7523  recexre  7678  rimul  7685  ltmul1  7692  mulap0  7744  mulcanapd  7751  suprzclex  8445  qbtwnre  9265  cvg1nlemres  9871  cvg1n  9872  recvguniq  9881  resqrexlemoverl  9907  resqrexlemex  9911  fimaxre2  10109  climge0  10163  climrecvg1n  10185  oexpneg  10276  zsupcllemex  10342  zssinfcl  10344  bezoutlemnewy  10385  bezoutlemstep  10386  dfgcd3  10399  bezout  10400  qdencn  10785