Theorem exlimddv 1954

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie2 1547  ax-17 1579

This proof depends on definitions:  df-bi 117

This theorem is used by:  fvmptdv2  5795  tfrlemi14d  6604  tfrexlem  6605  tfr1onlemres  6620  tfrcllemres  6633  tfrcldm  6634  erref  6827  1dom1el  7107  en2  7112  en2m  7113  xpdom2  7129  dom0  7138  xpen  7145  mapdom1g  7147  phplem4dom  7163  phplem4on  7169  fidceq  7171  dif1en  7183  fin0  7189  fin0or  7190  isinfinf  7201  eqsndc  7210  infm  7211  en2eqpr  7214  fiuni  7312  supelti  7342  djudom  7433  difinfsn  7440  enomnilem  7478  enmkvlem  7501  enwomnilem  7509  exmidfodomrlemim  7553  exmidaclem  7564  cc2lem  7632  cc3  7634  genpml  7884  genpmu  7885  ltexprlemm  7967  ltexprlemfl  7976  ltexprlemfu  7978  suplocsr  8176  axpre-suploc  8269  eqord1  8811  nn1suc  9323  nninfdcex  10672  zsupssdc  10673  seq3f1oleml  10953  zfz1isolem1  11292  eulerth  13011  4sqlem14  13183  4sqlem17  13186  4sqlem18  13187  ennnfonelemim  13315  exmidunben  13317  enctlem  13323  ctiunct  13331  unct  13333  omctfn  13334  omiunct  13335  relelbasov  13416  issubg2m  13992  gsump1  14157  gsumf1ofi  14160  gsummhmfi  14164  gsumressfi  14167  opprringb  14386  lmff  15350  txcn  15376  suplociccreex  15725  suplociccex  15726  wlkvtxiedg  16586  wlkvtxiedgg  16587  wlkreslem  16619  eulerpathum  16722  3dom  17018  subctctexmid  17030  exmidsbthrlem  17067  sbthom  17071