Theorem rexlimddv 2629

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2177  ∃wrex 2486

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2490  df-rex 2491

This theorem is referenced by:  disjiun  4045  nnsucpred  4672  tfrlemisucaccv  6423  tfrexlem  6432  tfr1onlemsucaccv  6439  tfrcllemsucaccv  6452  fict  6979  fidceq  6980  dif1enen  6991  php5fin  6993  fisbth  6994  fin0  6996  fin0or  6997  diffisn  7004  infnfi  7006  fientri3  7026  unsnfi  7030  unsnfidcex  7031  unsnfidcel  7032  fiuni  7094  ctmlemr  7224  ctssdccl  7227  fodjum  7262  fodju0  7263  exmidfodomrlemr  7325  exmidfodomrlemrALT  7326  cc2lem  7393  prarloclemarch2  7547  addlocpr  7664  nqprl  7679  nqpru  7680  appdiv0nq  7692  prmuloc  7694  mullocpr  7699  ltprordil  7717  ltaddpr  7725  ltexprlemopl  7729  ltexprlemopu  7731  ltexprlemloc  7735  ltexprlemrl  7738  ltexprlemru  7740  addcanprleml  7742  addcanprlemu  7743  ltaprlem  7746  ltaprg  7747  prplnqu  7748  recexprlemloc  7759  recexprlem1ssl  7761  recexprlem1ssu  7762  aptiprleml  7767  aptiprlemu  7768  ltmprr  7770  archpr  7771  cauappcvgprlemopl  7774  cauappcvgprlemopu  7776  cauappcvgprlemloc  7780  cauappcvgprlem1  7787  cauappcvgprlem2  7788  archrecpr  7792  caucvgprlemopl  7797  caucvgprlemopu  7799  caucvgprlemloc  7803  caucvgprlem2  7808  caucvgprprlemml  7822  caucvgprprlemmu  7823  caucvgprprlemopl  7825  caucvgprprlemopu  7827  caucvgprprlemloc  7831  caucvgprprlemexbt  7834  caucvgprprlem2  7838  suplocexprlemrl  7845  suplocexprlemmu  7846  suplocexprlemru  7847  suplocexprlemdisj  7848  suplocexprlemloc  7849  suplocexprlemex  7850  suplocexprlemub  7851  suplocexprlemlub  7852  prsrriota  7916  caucvgsrlemgt1  7923  caucvgsrlemoffres  7928  suplocsrlem  7936  rereceu  8017  recriota  8018  axarch  8019  axcaucvglemres  8027  axpre-suploclemres  8029  readdcan  8227  cnegex  8265  addcan  8267  addcan2  8268  negeu  8278  ltadd2  8507  recexre  8666  rimul  8673  ltmul1  8680  mulap0  8742  mulcanapd  8749  suprzclex  9486  zsupcllemex  10390  zssinfcl  10392  suprzubdc  10396  zsupssdc  10398  suprzcl2dc  10399  qbtwnre  10416  hashcl  10943  hashen  10946  fihashdom  10965  hashunlem  10966  hashun  10967  zfz1iso  11003  lencl  11015  sswrd  11020  cvg1nlemres  11366  cvg1n  11367  recvguniq  11376  resqrexlemoverl  11402  resqrexlemex  11406  fimaxre2  11608  climge0  11706  climrecvg1n  11729  fsum3cvg3  11777  expcnvre  11884  mertenslemub  11915  efcllem  12040  oexpneg  12258  bitsfzolem  12335  bitsfi  12338  bezoutlemnewy  12387  bezoutlemstep  12388  dfgcd3  12401  bezout  12402  isprm5lem  12533  ennnfonelemex  12855  ennnfonelemrnh  12857  ennnfonelemf1  12859  ennnfonelemrn  12860  ennnfonelemdm  12861  ennnfonelemnn0  12863  ctinfomlemom  12868  ctinf  12871  ctiunctlemfo  12880  nninfdclemcl  12889  nninfdc  12894  grpinvalem  13287  grprida  13289  grprcan  13439  mplsubgfilemcl  14531  restbasg  14710  cnpnei  14761  cnptopco  14764  xmettx  15052  metcnpi3  15059  mulcncf  15150  dedekindeulemuub  15159  dedekindeulemub  15160  dedekindeulemlu  15163  dedekindicclemuub  15168  dedekindicclemub  15169  dedekindicclemlu  15172  dedekindicc  15175  ivthinclemlopn  15178  ivthinclemuopn  15180  ivthreinc  15187  ivthdichlem  15193  limcimolemlt  15206  limcimo  15207  limccnp2cntop  15219  reeff1oleme  15314  eflt  15317  bj-charfunr  15880  qdencn  16101  trilpolemlt1  16115  nconstwlpolemgt0  16138