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  5724  tfrlemi14d  6479  tfrexlem  6480  tfr1onlemres  6495  tfrcllemres  6508  tfrcldm  6509  erref  6700  en2  6973  en2m  6974  xpdom2  6990  dom0  6999  xpen  7006  mapdom1g  7008  phplem4dom  7023  phplem4on  7029  fidceq  7031  dif1en  7041  fin0  7047  fin0or  7048  isinfinf  7059  infm  7066  en2eqpr  7069  fiuni  7145  supelti  7169  djudom  7260  difinfsn  7267  enomnilem  7305  enmkvlem  7328  enwomnilem  7336  exmidfodomrlemim  7379  exmidaclem  7390  cc2lem  7452  cc3  7454  genpml  7704  genpmu  7705  ltexprlemm  7787  ltexprlemfl  7796  ltexprlemfu  7798  suplocsr  7996  axpre-suploc  8089  eqord1  8630  nn1suc  9129  nninfdcex  10457  zsupssdc  10458  seq3f1oleml  10738  zfz1isolem1  11062  eulerth  12755  4sqlem14  12927  4sqlem17  12930  4sqlem18  12931  ennnfonelemim  12995  exmidunben  12997  enctlem  13003  ctiunct  13011  unct  13013  omctfn  13014  omiunct  13015  relelbasov  13095  issubg2m  13726  lmff  14923  txcn  14949  suplociccreex  15298  suplociccex  15299  wlkvtxiedg  16056  wlkvtxiedgg  16057  1dom1el  16354  subctctexmid  16366  exmidsbthrlem  16390  sbthom  16394