Theorem exlimddv 1886

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

Syntax hints:   -> wi 4   /\ wa 103   E.wex 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie2 1482  ax-17 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  fvmptdv2  5575  tfrlemi14d  6301  tfrexlem  6302  tfr1onlemres  6317  tfrcllemres  6330  tfrcldm  6331  erref  6521  xpdom2  6797  dom0  6804  xpen  6811  mapdom1g  6813  phplem4dom  6828  phplem4on  6833  fidceq  6835  dif1en  6845  fin0  6851  fin0or  6852  isinfinf  6863  infm  6870  en2eqpr  6873  fiuni  6943  supelti  6967  djudom  7058  difinfsn  7065  enomnilem  7102  enmkvlem  7125  enwomnilem  7133  exmidfodomrlemim  7157  exmidaclem  7164  cc2lem  7207  cc3  7209  genpml  7458  genpmu  7459  ltexprlemm  7541  ltexprlemfl  7550  ltexprlemfu  7552  suplocsr  7750  axpre-suploc  7843  eqord1  8381  nn1suc  8876  seq3f1oleml  10438  zfz1isolem1  10753  nninfdcex  11886  zsupssdc  11887  eulerth  12165  ennnfonelemim  12357  exmidunben  12359  enctlem  12365  ctiunct  12373  unct  12375  omctfn  12376  omiunct  12377  lmff  12889  txcn  12915  suplociccreex  13242  suplociccex  13243  subctctexmid  13881  exmidsbthrlem  13901  sbthom  13905