Theorem rexlimddv 2552

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1480  ∃wrex 2415

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-i5r 1515

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2419  df-rex 2420

This theorem is referenced by:  disjiun  3919  nnsucpred  4525  grprinvlem  5958  grpridd  5960  tfrlemisucaccv  6215  tfrexlem  6224  tfr1onlemsucaccv  6231  tfrcllemsucaccv  6244  fict  6755  fidceq  6756  dif1enen  6767  php5fin  6769  fisbth  6770  fin0  6772  fin0or  6773  diffisn  6780  infnfi  6782  fientri3  6796  unsnfi  6800  unsnfidcex  6801  unsnfidcel  6802  fiuni  6859  ctmlemr  6986  ctssdccl  6989  fodjum  7011  fodju0  7012  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  prarloclemarch2  7220  addlocpr  7337  nqprl  7352  nqpru  7353  appdiv0nq  7365  prmuloc  7367  mullocpr  7372  ltprordil  7390  ltaddpr  7398  ltexprlemopl  7402  ltexprlemopu  7404  ltexprlemloc  7408  ltexprlemrl  7411  ltexprlemru  7413  addcanprleml  7415  addcanprlemu  7416  ltaprlem  7419  ltaprg  7420  prplnqu  7421  recexprlemloc  7432  recexprlem1ssl  7434  recexprlem1ssu  7435  aptiprleml  7440  aptiprlemu  7441  ltmprr  7443  archpr  7444  cauappcvgprlemopl  7447  cauappcvgprlemopu  7449  cauappcvgprlemloc  7453  cauappcvgprlem1  7460  cauappcvgprlem2  7461  archrecpr  7465  caucvgprlemopl  7470  caucvgprlemopu  7472  caucvgprlemloc  7476  caucvgprlem2  7481  caucvgprprlemml  7495  caucvgprprlemmu  7496  caucvgprprlemopl  7498  caucvgprprlemopu  7500  caucvgprprlemloc  7504  caucvgprprlemexbt  7507  caucvgprprlem2  7511  suplocexprlemrl  7518  suplocexprlemmu  7519  suplocexprlemru  7520  suplocexprlemdisj  7521  suplocexprlemloc  7522  suplocexprlemex  7523  suplocexprlemub  7524  suplocexprlemlub  7525  prsrriota  7589  caucvgsrlemgt1  7596  caucvgsrlemoffres  7601  suplocsrlem  7609  rereceu  7690  recriota  7691  axarch  7692  axcaucvglemres  7700  axpre-suploclemres  7702  readdcan  7895  cnegex  7933  addcan  7935  addcan2  7936  negeu  7946  ltadd2  8174  recexre  8333  rimul  8340  ltmul1  8347  mulap0  8408  mulcanapd  8415  suprzclex  9142  qbtwnre  10027  hashcl  10520  hashen  10523  fihashdom  10542  hashunlem  10543  hashun  10544  zfz1iso  10577  cvg1nlemres  10750  cvg1n  10751  recvguniq  10760  resqrexlemoverl  10786  resqrexlemex  10790  fimaxre2  10991  climge0  11087  climrecvg1n  11110  fsum3cvg3  11158  expcnvre  11265  mertenslemub  11296  efcllem  11354  oexpneg  11563  zsupcllemex  11628  zssinfcl  11630  bezoutlemnewy  11673  bezoutlemstep  11674  dfgcd3  11687  bezout  11688  ennnfonelemex  11916  ennnfonelemrnh  11918  ennnfonelemf1  11920  ennnfonelemrn  11921  ennnfonelemdm  11922  ennnfonelemnn0  11924  ctinfomlemom  11929  ctinf  11932  ctiunctlemfo  11941  restbasg  12326  cnpnei  12377  cnptopco  12380  xmettx  12668  metcnpi3  12675  mulcncf  12749  dedekindeulemuub  12753  dedekindeulemub  12754  dedekindeulemlu  12757  dedekindicclemuub  12762  dedekindicclemub  12763  dedekindicclemlu  12766  dedekindicc  12769  ivthinclemlopn  12772  ivthinclemuopn  12774  limcimolemlt  12791  limcimo  12792  limccnp2cntop  12804  qdencn  13211  trilpolemlt1  13223