Theorem exlimddv 1947

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie2 1543  ax-17 1575

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5745  tfrlemi14d  6542  tfrexlem  6543  tfr1onlemres  6558  tfrcllemres  6571  tfrcldm  6572  erref  6765  1dom1el  7036  en2  7041  en2m  7042  xpdom2  7058  dom0  7067  xpen  7074  mapdom1g  7076  phplem4dom  7091  phplem4on  7097  fidceq  7099  dif1en  7111  fin0  7117  fin0or  7118  isinfinf  7129  eqsndc  7138  infm  7139  en2eqpr  7142  fiuni  7237  supelti  7261  djudom  7352  difinfsn  7359  enomnilem  7397  enmkvlem  7420  enwomnilem  7428  exmidfodomrlemim  7472  exmidaclem  7483  cc2lem  7545  cc3  7547  genpml  7797  genpmu  7798  ltexprlemm  7880  ltexprlemfl  7889  ltexprlemfu  7891  suplocsr  8089  axpre-suploc  8182  eqord1  8722  nn1suc  9221  nninfdcex  10560  zsupssdc  10561  seq3f1oleml  10841  zfz1isolem1  11167  eulerth  12885  4sqlem14  13057  4sqlem17  13060  4sqlem18  13061  ennnfonelemim  13125  exmidunben  13127  enctlem  13133  ctiunct  13141  unct  13143  omctfn  13144  omiunct  13145  relelbasov  13225  issubg2m  13856  lmff  15060  txcn  15086  suplociccreex  15435  suplociccex  15436  wlkvtxiedg  16286  wlkvtxiedgg  16287  wlkreslem  16319  eulerpathum  16422  3dom  16708  subctctexmid  16722  exmidsbthrlem  16750  sbthom  16754  gfsump1  16815