Theorem rexlimddv 2599

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  ∃wrex 2456

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  disjiun  4000  nnsucpred  4618  tfrlemisucaccv  6329  tfrexlem  6338  tfr1onlemsucaccv  6345  tfrcllemsucaccv  6358  fict  6871  fidceq  6872  dif1enen  6883  php5fin  6885  fisbth  6886  fin0  6888  fin0or  6889  diffisn  6896  infnfi  6898  fientri3  6917  unsnfi  6921  unsnfidcex  6922  unsnfidcel  6923  fiuni  6980  ctmlemr  7110  ctssdccl  7113  fodjum  7147  fodju0  7148  exmidfodomrlemr  7204  exmidfodomrlemrALT  7205  cc2lem  7268  prarloclemarch2  7421  addlocpr  7538  nqprl  7553  nqpru  7554  appdiv0nq  7566  prmuloc  7568  mullocpr  7573  ltprordil  7591  ltaddpr  7599  ltexprlemopl  7603  ltexprlemopu  7605  ltexprlemloc  7609  ltexprlemrl  7612  ltexprlemru  7614  addcanprleml  7616  addcanprlemu  7617  ltaprlem  7620  ltaprg  7621  prplnqu  7622  recexprlemloc  7633  recexprlem1ssl  7635  recexprlem1ssu  7636  aptiprleml  7641  aptiprlemu  7642  ltmprr  7644  archpr  7645  cauappcvgprlemopl  7648  cauappcvgprlemopu  7650  cauappcvgprlemloc  7654  cauappcvgprlem1  7661  cauappcvgprlem2  7662  archrecpr  7666  caucvgprlemopl  7671  caucvgprlemopu  7673  caucvgprlemloc  7677  caucvgprlem2  7682  caucvgprprlemml  7696  caucvgprprlemmu  7697  caucvgprprlemopl  7699  caucvgprprlemopu  7701  caucvgprprlemloc  7705  caucvgprprlemexbt  7708  caucvgprprlem2  7712  suplocexprlemrl  7719  suplocexprlemmu  7720  suplocexprlemru  7721  suplocexprlemdisj  7722  suplocexprlemloc  7723  suplocexprlemex  7724  suplocexprlemub  7725  suplocexprlemlub  7726  prsrriota  7790  caucvgsrlemgt1  7797  caucvgsrlemoffres  7802  suplocsrlem  7810  rereceu  7891  recriota  7892  axarch  7893  axcaucvglemres  7901  axpre-suploclemres  7903  readdcan  8100  cnegex  8138  addcan  8140  addcan2  8141  negeu  8151  ltadd2  8379  recexre  8538  rimul  8545  ltmul1  8552  mulap0  8614  mulcanapd  8621  suprzclex  9354  qbtwnre  10260  hashcl  10764  hashen  10767  fihashdom  10786  hashunlem  10787  hashun  10788  zfz1iso  10824  cvg1nlemres  10997  cvg1n  10998  recvguniq  11007  resqrexlemoverl  11033  resqrexlemex  11037  fimaxre2  11238  climge0  11336  climrecvg1n  11359  fsum3cvg3  11407  expcnvre  11514  mertenslemub  11545  efcllem  11670  oexpneg  11885  zsupcllemex  11950  zssinfcl  11952  suprzubdc  11956  zsupssdc  11958  suprzcl2dc  11959  bezoutlemnewy  12000  bezoutlemstep  12001  dfgcd3  12014  bezout  12015  isprm5lem  12144  ennnfonelemex  12418  ennnfonelemrnh  12420  ennnfonelemf1  12422  ennnfonelemrn  12423  ennnfonelemdm  12424  ennnfonelemnn0  12426  ctinfomlemom  12431  ctinf  12434  ctiunctlemfo  12443  nninfdclemcl  12452  nninfdc  12457  grprinvlem  12810  grpridd  12812  grprcan  12916  restbasg  13808  cnpnei  13859  cnptopco  13862  xmettx  14150  metcnpi3  14157  mulcncf  14231  dedekindeulemuub  14235  dedekindeulemub  14236  dedekindeulemlu  14239  dedekindicclemuub  14244  dedekindicclemub  14245  dedekindicclemlu  14248  dedekindicc  14251  ivthinclemlopn  14254  ivthinclemuopn  14256  limcimolemlt  14273  limcimo  14274  limccnp2cntop  14286  reeff1oleme  14333  eflt  14336  bj-charfunr  14702  qdencn  14916  trilpolemlt1  14930  nconstwlpolemgt0  14953