Theorem exlimddv 1945

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

Syntax hints:   -> wi 4   /\ wa 104   E.wex 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie2 1540  ax-17 1572

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5726  tfrlemi14d  6485  tfrexlem  6486  tfr1onlemres  6501  tfrcllemres  6514  tfrcldm  6515  erref  6708  en2  6981  en2m  6982  xpdom2  6998  dom0  7007  xpen  7014  mapdom1g  7016  phplem4dom  7031  phplem4on  7037  fidceq  7039  dif1en  7049  fin0  7055  fin0or  7056  isinfinf  7067  eqsndc  7076  infm  7077  en2eqpr  7080  fiuni  7156  supelti  7180  djudom  7271  difinfsn  7278  enomnilem  7316  enmkvlem  7339  enwomnilem  7347  exmidfodomrlemim  7390  exmidaclem  7401  cc2lem  7463  cc3  7465  genpml  7715  genpmu  7716  ltexprlemm  7798  ltexprlemfl  7807  ltexprlemfu  7809  suplocsr  8007  axpre-suploc  8100  eqord1  8641  nn1suc  9140  nninfdcex  10469  zsupssdc  10470  seq3f1oleml  10750  zfz1isolem1  11075  eulerth  12771  4sqlem14  12943  4sqlem17  12946  4sqlem18  12947  ennnfonelemim  13011  exmidunben  13013  enctlem  13019  ctiunct  13027  unct  13029  omctfn  13030  omiunct  13031  relelbasov  13111  issubg2m  13742  lmff  14939  txcn  14965  suplociccreex  15314  suplociccex  15315  wlkvtxiedg  16091  wlkvtxiedgg  16092  wlkreslem  16122  1dom1el  16437  3dom  16439  subctctexmid  16453  exmidsbthrlem  16478  sbthom  16482