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 )

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

This theorem was proved from 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 theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5789  tfrlemi14d  6594  tfrexlem  6595  tfr1onlemres  6610  tfrcllemres  6623  tfrcldm  6624  erref  6817  1dom1el  7097  en2  7102  en2m  7103  xpdom2  7119  dom0  7128  xpen  7135  mapdom1g  7137  phplem4dom  7153  phplem4on  7159  fidceq  7161  dif1en  7173  fin0  7179  fin0or  7180  isinfinf  7191  eqsndc  7200  infm  7201  en2eqpr  7204  fiuni  7302  supelti  7332  djudom  7423  difinfsn  7430  enomnilem  7468  enmkvlem  7491  enwomnilem  7499  exmidfodomrlemim  7543  exmidaclem  7554  cc2lem  7622  cc3  7624  genpml  7874  genpmu  7875  ltexprlemm  7957  ltexprlemfl  7966  ltexprlemfu  7968  suplocsr  8166  axpre-suploc  8259  eqord1  8801  nn1suc  9302  nninfdcex  10650  zsupssdc  10651  seq3f1oleml  10931  zfz1isolem1  11270  eulerth  12989  4sqlem14  13161  4sqlem17  13164  4sqlem18  13165  ennnfonelemim  13293  exmidunben  13295  enctlem  13301  ctiunct  13309  unct  13311  omctfn  13312  omiunct  13313  relelbasov  13393  issubg2m  13969  gsump1  14134  gsumf1ofi  14137  gsummhmfi  14141  gsumressfi  14144  opprringb  14359  lmff  15273  txcn  15299  suplociccreex  15648  suplociccex  15649  wlkvtxiedg  16500  wlkvtxiedgg  16501  wlkreslem  16533  eulerpathum  16636  3dom  16932  subctctexmid  16944  exmidsbthrlem  16972  sbthom  16976