Theorem exlimddv 1948

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 1868	. 2 |- ( ph -> ( E. x ps -> ch ) )
5	1, 4	mpd 13	1 |- ( ph -> ch )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie2 1543  ax-17 1575

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5767  tfrlemi14d  6564  tfrexlem  6565  tfr1onlemres  6580  tfrcllemres  6593  tfrcldm  6594  erref  6787  1dom1el  7060  en2  7065  en2m  7066  xpdom2  7082  dom0  7091  xpen  7098  mapdom1g  7100  phplem4dom  7116  phplem4on  7122  fidceq  7124  dif1en  7136  fin0  7142  fin0or  7143  isinfinf  7154  eqsndc  7163  infm  7164  en2eqpr  7167  fiuni  7265  supelti  7293  djudom  7384  difinfsn  7391  enomnilem  7429  enmkvlem  7452  enwomnilem  7460  exmidfodomrlemim  7504  exmidaclem  7515  cc2lem  7580  cc3  7582  genpml  7832  genpmu  7833  ltexprlemm  7915  ltexprlemfl  7924  ltexprlemfu  7926  suplocsr  8124  axpre-suploc  8217  eqord1  8757  nn1suc  9256  nninfdcex  10597  zsupssdc  10598  seq3f1oleml  10878  zfz1isolem1  11212  eulerth  12930  4sqlem14  13102  4sqlem17  13105  4sqlem18  13106  ennnfonelemim  13175  exmidunben  13177  enctlem  13183  ctiunct  13191  unct  13193  omctfn  13194  omiunct  13195  relelbasov  13275  issubg2m  13906  lmff  15114  txcn  15140  suplociccreex  15489  suplociccex  15490  wlkvtxiedg  16340  wlkvtxiedgg  16341  wlkreslem  16373  eulerpathum  16476  3dom  16762  subctctexmid  16774  exmidsbthrlem  16802  sbthom  16806  gfsump1  16868