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  6499  tfrexlem  6500  tfr1onlemres  6515  tfrcllemres  6528  tfrcldm  6529  erref  6722  1dom1el  6993  en2  6998  en2m  6999  xpdom2  7015  dom0  7024  xpen  7031  mapdom1g  7033  phplem4dom  7048  phplem4on  7054  fidceq  7056  dif1en  7068  fin0  7074  fin0or  7075  isinfinf  7086  eqsndc  7095  infm  7096  en2eqpr  7099  fiuni  7177  supelti  7201  djudom  7292  difinfsn  7299  enomnilem  7337  enmkvlem  7360  enwomnilem  7368  exmidfodomrlemim  7412  exmidaclem  7423  cc2lem  7485  cc3  7487  genpml  7737  genpmu  7738  ltexprlemm  7820  ltexprlemfl  7829  ltexprlemfu  7831  suplocsr  8029  axpre-suploc  8122  eqord1  8663  nn1suc  9162  nninfdcex  10498  zsupssdc  10499  seq3f1oleml  10779  zfz1isolem1  11105  eulerth  12823  4sqlem14  12995  4sqlem17  12998  4sqlem18  12999  ennnfonelemim  13063  exmidunben  13065  enctlem  13071  ctiunct  13079  unct  13081  omctfn  13082  omiunct  13083  relelbasov  13163  issubg2m  13794  lmff  14992  txcn  15018  suplociccreex  15367  suplociccex  15368  wlkvtxiedg  16215  wlkvtxiedgg  16216  wlkreslem  16248  eulerpathum  16351  3dom  16638  subctctexmid  16652  exmidsbthrlem  16677  sbthom  16681  gfsump1  16738