Theorem rexlimddv 2673

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∃wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is used by:  disjiun  4125  nnsucpred  4766  tfrlemisucaccv  6601  tfrexlem  6610  tfr1onlemsucaccv  6617  tfrcllemsucaccv  6630  fict  7176  fidceq  7177  dif1enen  7190  php5fin  7192  fisbth  7193  fin0  7195  fin0or  7196  diffisn  7203  infnfi  7205  fidcen  7209  fientri3  7228  unsnfi  7232  unsnfidcex  7233  unsnfidcel  7234  fiuni  7317  ctmlemr  7454  ctssdccl  7457  fodjum  7492  fodju0  7493  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  cc2lem  7638  prarloclemarch2  7792  addlocpr  7909  nqprl  7924  nqpru  7925  appdiv0nq  7937  prmuloc  7939  mullocpr  7944  ltprordil  7962  ltaddpr  7970  ltexprlemopl  7974  ltexprlemopu  7976  ltexprlemloc  7980  ltexprlemrl  7983  ltexprlemru  7985  addcanprleml  7987  addcanprlemu  7988  ltaprlem  7991  ltaprg  7992  prplnqu  7993  recexprlemloc  8004  recexprlem1ssl  8006  recexprlem1ssu  8007  aptiprleml  8012  aptiprlemu  8013  ltmprr  8015  archpr  8016  cauappcvgprlemopl  8019  cauappcvgprlemopu  8021  cauappcvgprlemloc  8025  cauappcvgprlem1  8032  cauappcvgprlem2  8033  archrecpr  8037  caucvgprlemopl  8042  caucvgprlemopu  8044  caucvgprlemloc  8048  caucvgprlem2  8053  caucvgprprlemml  8067  caucvgprprlemmu  8068  caucvgprprlemopl  8070  caucvgprprlemopu  8072  caucvgprprlemloc  8076  caucvgprprlemexbt  8079  caucvgprprlem2  8083  suplocexprlemrl  8090  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemex  8095  suplocexprlemub  8096  suplocexprlemlub  8097  prsrriota  8161  caucvgsrlemgt1  8168  caucvgsrlemoffres  8173  suplocsrlem  8181  rereceu  8262  recriota  8263  axarch  8264  axcaucvglemres  8272  axpre-suploclemres  8274  readdcan  8473  cnegex  8511  addcan  8513  addcan2  8514  negeu  8524  ltadd2  8754  recexre  8914  rimul  8921  ltmul1  8928  mulap0  8990  mulcanapd  8997  suprzclex  9754  zsupcllemex  10679  zssinfcl  10681  suprzubdc  10687  zsupssdc  10689  suprzcl2dc  10690  qbtwnre  10707  hashcl  11241  hashen  11244  fihashdom  11264  hashunlem  11265  hashun  11266  zfz1iso  11314  lencl  11329  sswrd  11334  cvg1nlemres  11772  cvg1n  11773  recvguniq  11782  resqrexlemoverl  11808  resqrexlemex  11812  fimaxre2  12015  climge0  12115  climrecvg1n  12138  fsum3cvg3  12187  expcnvre  12294  mertenslemub  12325  efcllem  12450  oexpneg  12668  bitsfzolem  12745  bitsfi  12748  bezoutlemnewy  12797  bezoutlemstep  12798  dfgcd3  12811  bezout  12812  isprm5lem  12944  ballotfilemscl  13304  ballotfilemsle  13305  ennnfonelemex  13362  ennnfonelemrnh  13364  ennnfonelemf1  13366  ennnfonelemrn  13367  ennnfonelemdm  13368  ennnfonelemnn0  13370  ctinfomlemom  13375  ctinf  13378  ctiunctlemfo  13387  nninfdclemcl  13396  nninfdc  13401  grpinvalem  13763  grprida  13765  grprcan  13900  psrbaglefifi  15175  mvrclfi  15226  mplsubgfilemcl  15232  restbasg  15411  cnpnei  15462  cnptopco  15465  xmettx  15753  metcnpi3  15760  mulcncf  15851  dedekindeulemuub  15860  dedekindeulemub  15861  dedekindeulemlu  15864  dedekindicclemuub  15869  dedekindicclemub  15870  dedekindicclemlu  15873  dedekindicc  15876  ivthinclemlopn  15879  ivthinclemuopn  15881  ivthreinc  15888  ivthdichlem  15894  limcimolemlt  15907  limcimo  15908  limccnp2cntop  15920  reeff1oleme  16015  eflt  16018  upgredg  16607  bj-charfunr  17058  qdencn  17295  trilpolemlt1  17314  nconstwlpolemgt0  17338