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  8812  nn1suc  9325  nninfdcex  10682  zsupssdc  10683  seq3f1oleml  10966  zfz1isolem1  11306  eulerth  13031  4sqlem14  13203  4sqlem17  13206  4sqlem18  13207  ennnfonelemim  13364  exmidunben  13366  enctlem  13372  ctiunct  13380  unct  13382  omctfn  13383  omiunct  13384  relelbasov  13465  issubg2m  14041  gsump1  14206  gsumf1ofi  14209  gsummhmfi  14213  gsumressfi  14216  opprringb  14435  lmff  15399  txcn  15425  suplociccreex  15774  suplociccex  15775  wlkvtxiedg  16684  wlkvtxiedgg  16685  wlkreslem  16717  eulerpathum  16820  3dom  17116  subctctexmid  17128  exmidsbthrlem  17165  sbthom  17169