Theorem rexlimddv 2656

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  ∃wrex 2512

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516  df-rex 2517

This theorem is referenced by:  disjiun  4088  nnsucpred  4721  tfrlemisucaccv  6534  tfrexlem  6543  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  fict  7098  fidceq  7099  dif1enen  7112  php5fin  7114  fisbth  7115  fin0  7117  fin0or  7118  diffisn  7125  infnfi  7127  fidcen  7131  fientri3  7150  unsnfi  7154  unsnfidcex  7155  unsnfidcel  7156  fiuni  7220  ctmlemr  7350  ctssdccl  7353  fodjum  7388  fodju0  7389  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  cc2lem  7528  prarloclemarch2  7682  addlocpr  7799  nqprl  7814  nqpru  7815  appdiv0nq  7827  prmuloc  7829  mullocpr  7834  ltprordil  7852  ltaddpr  7860  ltexprlemopl  7864  ltexprlemopu  7866  ltexprlemloc  7870  ltexprlemrl  7873  ltexprlemru  7875  addcanprleml  7877  addcanprlemu  7878  ltaprlem  7881  ltaprg  7882  prplnqu  7883  recexprlemloc  7894  recexprlem1ssl  7896  recexprlem1ssu  7897  aptiprleml  7902  aptiprlemu  7903  ltmprr  7905  archpr  7906  cauappcvgprlemopl  7909  cauappcvgprlemopu  7911  cauappcvgprlemloc  7915  cauappcvgprlem1  7922  cauappcvgprlem2  7923  archrecpr  7927  caucvgprlemopl  7932  caucvgprlemopu  7934  caucvgprlemloc  7938  caucvgprlem2  7943  caucvgprprlemml  7957  caucvgprprlemmu  7958  caucvgprprlemopl  7960  caucvgprprlemopu  7962  caucvgprprlemloc  7966  caucvgprprlemexbt  7969  caucvgprprlem2  7973  suplocexprlemrl  7980  suplocexprlemmu  7981  suplocexprlemru  7982  suplocexprlemdisj  7983  suplocexprlemloc  7984  suplocexprlemex  7985  suplocexprlemub  7986  suplocexprlemlub  7987  prsrriota  8051  caucvgsrlemgt1  8058  caucvgsrlemoffres  8063  suplocsrlem  8071  rereceu  8152  recriota  8153  axarch  8154  axcaucvglemres  8162  axpre-suploclemres  8164  readdcan  8361  cnegex  8399  addcan  8401  addcan2  8402  negeu  8412  ltadd2  8641  recexre  8800  rimul  8807  ltmul1  8814  mulap0  8876  mulcanapd  8883  suprzclex  9622  zsupcllemex  10536  zssinfcl  10538  suprzubdc  10542  zsupssdc  10544  suprzcl2dc  10545  qbtwnre  10562  hashcl  11089  hashen  11092  fihashdom  11112  hashunlem  11113  hashun  11114  zfz1iso  11151  lencl  11166  sswrd  11171  cvg1nlemres  11608  cvg1n  11609  recvguniq  11618  resqrexlemoverl  11644  resqrexlemex  11648  fimaxre2  11850  climge0  11948  climrecvg1n  11971  fsum3cvg3  12020  expcnvre  12127  mertenslemub  12158  efcllem  12283  oexpneg  12501  bitsfzolem  12578  bitsfi  12581  bezoutlemnewy  12630  bezoutlemstep  12631  dfgcd3  12644  bezout  12645  isprm5lem  12776  ennnfonelemex  13098  ennnfonelemrnh  13100  ennnfonelemf1  13102  ennnfonelemrn  13103  ennnfonelemdm  13104  ennnfonelemnn0  13106  ctinfomlemom  13111  ctinf  13114  ctiunctlemfo  13123  nninfdclemcl  13132  nninfdc  13137  grpinvalem  13531  grprida  13533  grprcan  13683  mplsubgfilemcl  14783  restbasg  14962  cnpnei  15013  cnptopco  15016  xmettx  15304  metcnpi3  15311  mulcncf  15402  dedekindeulemuub  15411  dedekindeulemub  15412  dedekindeulemlu  15415  dedekindicclemuub  15420  dedekindicclemub  15421  dedekindicclemlu  15424  dedekindicc  15427  ivthinclemlopn  15430  ivthinclemuopn  15432  ivthreinc  15439  ivthdichlem  15445  limcimolemlt  15458  limcimo  15459  limccnp2cntop  15471  reeff1oleme  15566  eflt  15569  upgredg  16068  bj-charfunr  16509  qdencn  16738  trilpolemlt1  16756  nconstwlpolemgt0  16780