Theorem exlimddv 1947

Description: Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)

Hypotheses

Ref	Expression
exlimddv.1	|- ( ph -> E. x ps )
exlimddv.2	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
exlimddv	|- ( ph -> ch )

Distinct variable groups:   ch, x   ph, x

Allowed substitution hint:   ps( x)

Proof of Theorem exlimddv

Step	Hyp	Ref	Expression
1		exlimddv.1	. 2 |- ( ph -> E. x ps )
2		exlimddv.2	. . . 4 |- ( ( ph /\ ps ) -> ch )
3	2	ex 115	. . 3 |- ( ph -> ( ps -> ch ) )
4	3	exlimdv 1867	. 2 |- ( ph -> ( E. x ps -> ch ) )
5	1, 4	mpd 13	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 104   E.wex 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie2 1542  ax-17 1574

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5736  tfrlemi14d  6498  tfrexlem  6499  tfr1onlemres  6514  tfrcllemres  6527  tfrcldm  6528  erref  6721  1dom1el  6992  en2  6997  en2m  6998  xpdom2  7014  dom0  7023  xpen  7030  mapdom1g  7032  phplem4dom  7047  phplem4on  7053  fidceq  7055  dif1en  7067  fin0  7073  fin0or  7074  isinfinf  7085  eqsndc  7094  infm  7095  en2eqpr  7098  fiuni  7176  supelti  7200  djudom  7291  difinfsn  7298  enomnilem  7336  enmkvlem  7359  enwomnilem  7367  exmidfodomrlemim  7411  exmidaclem  7422  cc2lem  7484  cc3  7486  genpml  7736  genpmu  7737  ltexprlemm  7819  ltexprlemfl  7828  ltexprlemfu  7830  suplocsr  8028  axpre-suploc  8121  eqord1  8662  nn1suc  9161  nninfdcex  10496  zsupssdc  10497  seq3f1oleml  10777  zfz1isolem1  11103  eulerth  12804  4sqlem14  12976  4sqlem17  12979  4sqlem18  12980  ennnfonelemim  13044  exmidunben  13046  enctlem  13052  ctiunct  13060  unct  13062  omctfn  13063  omiunct  13064  relelbasov  13144  issubg2m  13775  lmff  14972  txcn  14998  suplociccreex  15347  suplociccex  15348  wlkvtxiedg  16195  wlkvtxiedgg  16196  wlkreslem  16228  3dom  16587  subctctexmid  16601  exmidsbthrlem  16626  sbthom  16630