Theorem exlimddv 1950

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  5772  tfrlemi14d  6577  tfrexlem  6578  tfr1onlemres  6593  tfrcllemres  6606  tfrcldm  6607  erref  6800  1dom1el  7073  en2  7078  en2m  7079  xpdom2  7095  dom0  7104  xpen  7111  mapdom1g  7113  phplem4dom  7129  phplem4on  7135  fidceq  7137  dif1en  7149  fin0  7155  fin0or  7156  isinfinf  7167  eqsndc  7176  infm  7177  en2eqpr  7180  fiuni  7278  supelti  7306  djudom  7397  difinfsn  7404  enomnilem  7442  enmkvlem  7465  enwomnilem  7473  exmidfodomrlemim  7517  exmidaclem  7528  cc2lem  7596  cc3  7598  genpml  7848  genpmu  7849  ltexprlemm  7931  ltexprlemfl  7940  ltexprlemfu  7942  suplocsr  8140  axpre-suploc  8233  eqord1  8774  nn1suc  9273  nninfdcex  10621  zsupssdc  10622  seq3f1oleml  10902  zfz1isolem1  11237  eulerth  12955  4sqlem14  13127  4sqlem17  13130  4sqlem18  13131  ennnfonelemim  13259  exmidunben  13261  enctlem  13267  ctiunct  13275  unct  13277  omctfn  13278  omiunct  13279  relelbasov  13359  issubg2m  13942  gfsump1  14108  opprringb  14324  lmff  15240  txcn  15266  suplociccreex  15615  suplociccex  15616  wlkvtxiedg  16466  wlkvtxiedgg  16467  wlkreslem  16499  eulerpathum  16602  3dom  16888  subctctexmid  16900  exmidsbthrlem  16928  sbthom  16932