Theorem rexlimddv 2507

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1445  ∃wrex 2371

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-4 1452  ax-17 1471  ax-ial 1479  ax-i5r 1480

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-ral 2375  df-rex 2376

This theorem is referenced by:  disjiun  3862  grprinvlem  5877  grpridd  5879  tfrlemisucaccv  6128  tfrexlem  6137  tfr1onlemsucaccv  6144  tfrcllemsucaccv  6157  fict  6664  fidceq  6665  dif1enen  6676  php5fin  6678  fisbth  6679  fin0  6681  fin0or  6682  diffisn  6689  infnfi  6691  fientri3  6705  unsnfi  6709  unsnfidcex  6710  unsnfidcel  6711  ctmlemr  6870  fodjum  6889  fodju0  6890  exmidfodomrlemr  6925  exmidfodomrlemrALT  6926  prarloclemarch2  7075  addlocpr  7192  nqprl  7207  nqpru  7208  appdiv0nq  7220  prmuloc  7222  mullocpr  7227  ltprordil  7245  ltaddpr  7253  ltexprlemopl  7257  ltexprlemopu  7259  ltexprlemloc  7263  ltexprlemrl  7266  ltexprlemru  7268  addcanprleml  7270  addcanprlemu  7271  ltaprlem  7274  ltaprg  7275  prplnqu  7276  recexprlemloc  7287  recexprlem1ssl  7289  recexprlem1ssu  7290  aptiprleml  7295  aptiprlemu  7296  ltmprr  7298  archpr  7299  cauappcvgprlemopl  7302  cauappcvgprlemopu  7304  cauappcvgprlemloc  7308  cauappcvgprlem1  7315  cauappcvgprlem2  7316  archrecpr  7320  caucvgprlemopl  7325  caucvgprlemopu  7327  caucvgprlemloc  7331  caucvgprlem2  7336  caucvgprprlemml  7350  caucvgprprlemmu  7351  caucvgprprlemopl  7353  caucvgprprlemopu  7355  caucvgprprlemloc  7359  caucvgprprlemexbt  7362  caucvgprprlem2  7366  prsrriota  7430  caucvgsrlemgt1  7437  caucvgsrlemoffres  7442  rereceu  7521  recriota  7522  axarch  7523  axcaucvglemres  7531  readdcan  7719  cnegex  7757  addcan  7759  addcan2  7760  negeu  7770  ltadd2  7994  recexre  8152  rimul  8159  ltmul1  8166  mulap0  8220  mulcanapd  8227  suprzclex  8943  qbtwnre  9817  hashcl  10304  hashen  10307  fihashdom  10326  hashunlem  10327  hashun  10328  zfz1iso  10361  cvg1nlemres  10533  cvg1n  10534  recvguniq  10543  resqrexlemoverl  10569  resqrexlemex  10573  fimaxre2  10773  climge0  10868  climrecvg1n  10891  fsum3cvg3  10939  expcnvre  11046  mertenslemub  11077  efcllem  11098  oexpneg  11304  zsupcllemex  11369  zssinfcl  11371  bezoutlemnewy  11412  bezoutlemstep  11413  dfgcd3  11426  bezout  11427  restbasg  12020  cnpnei  12070  cnptopco  12073  metcnpi3  12299  mulcncf  12354  nnsucpred  12596  qdencn  12620