Theorem rexlimddv 2619

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  ∃wrex 2476

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-i5r 1549

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480  df-rex 2481

This theorem is referenced by:  disjiun  4029  nnsucpred  4654  tfrlemisucaccv  6392  tfrexlem  6401  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  fict  6938  fidceq  6939  dif1enen  6950  php5fin  6952  fisbth  6953  fin0  6955  fin0or  6956  diffisn  6963  infnfi  6965  fientri3  6985  unsnfi  6989  unsnfidcex  6990  unsnfidcel  6991  fiuni  7053  ctmlemr  7183  ctssdccl  7186  fodjum  7221  fodju0  7222  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  cc2lem  7351  prarloclemarch2  7505  addlocpr  7622  nqprl  7637  nqpru  7638  appdiv0nq  7650  prmuloc  7652  mullocpr  7657  ltprordil  7675  ltaddpr  7683  ltexprlemopl  7687  ltexprlemopu  7689  ltexprlemloc  7693  ltexprlemrl  7696  ltexprlemru  7698  addcanprleml  7700  addcanprlemu  7701  ltaprlem  7704  ltaprg  7705  prplnqu  7706  recexprlemloc  7717  recexprlem1ssl  7719  recexprlem1ssu  7720  aptiprleml  7725  aptiprlemu  7726  ltmprr  7728  archpr  7729  cauappcvgprlemopl  7732  cauappcvgprlemopu  7734  cauappcvgprlemloc  7738  cauappcvgprlem1  7745  cauappcvgprlem2  7746  archrecpr  7750  caucvgprlemopl  7755  caucvgprlemopu  7757  caucvgprlemloc  7761  caucvgprlem2  7766  caucvgprprlemml  7780  caucvgprprlemmu  7781  caucvgprprlemopl  7783  caucvgprprlemopu  7785  caucvgprprlemloc  7789  caucvgprprlemexbt  7792  caucvgprprlem2  7796  suplocexprlemrl  7803  suplocexprlemmu  7804  suplocexprlemru  7805  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemex  7808  suplocexprlemub  7809  suplocexprlemlub  7810  prsrriota  7874  caucvgsrlemgt1  7881  caucvgsrlemoffres  7886  suplocsrlem  7894  rereceu  7975  recriota  7976  axarch  7977  axcaucvglemres  7985  axpre-suploclemres  7987  readdcan  8185  cnegex  8223  addcan  8225  addcan2  8226  negeu  8236  ltadd2  8465  recexre  8624  rimul  8631  ltmul1  8638  mulap0  8700  mulcanapd  8707  suprzclex  9443  zsupcllemex  10339  zssinfcl  10341  suprzubdc  10345  zsupssdc  10347  suprzcl2dc  10348  qbtwnre  10365  hashcl  10892  hashen  10895  fihashdom  10914  hashunlem  10915  hashun  10916  zfz1iso  10952  lencl  10958  sswrd  10963  cvg1nlemres  11169  cvg1n  11170  recvguniq  11179  resqrexlemoverl  11205  resqrexlemex  11209  fimaxre2  11411  climge0  11509  climrecvg1n  11532  fsum3cvg3  11580  expcnvre  11687  mertenslemub  11718  efcllem  11843  oexpneg  12061  bitsfzolem  12138  bitsfi  12141  bezoutlemnewy  12190  bezoutlemstep  12191  dfgcd3  12204  bezout  12205  isprm5lem  12336  ennnfonelemex  12658  ennnfonelemrnh  12660  ennnfonelemf1  12662  ennnfonelemrn  12663  ennnfonelemdm  12664  ennnfonelemnn0  12666  ctinfomlemom  12671  ctinf  12674  ctiunctlemfo  12683  nninfdclemcl  12692  nninfdc  12697  grpinvalem  13089  grprida  13091  grprcan  13241  mplsubgfilemcl  14333  restbasg  14512  cnpnei  14563  cnptopco  14566  xmettx  14854  metcnpi3  14861  mulcncf  14952  dedekindeulemuub  14961  dedekindeulemub  14962  dedekindeulemlu  14965  dedekindicclemuub  14970  dedekindicclemub  14971  dedekindicclemlu  14974  dedekindicc  14977  ivthinclemlopn  14980  ivthinclemuopn  14982  ivthreinc  14989  ivthdichlem  14995  limcimolemlt  15008  limcimo  15009  limccnp2cntop  15021  reeff1oleme  15116  eflt  15119  bj-charfunr  15564  qdencn  15784  trilpolemlt1  15798  nconstwlpolemgt0  15821