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  5732  tfrlemi14d  6494  tfrexlem  6495  tfr1onlemres  6510  tfrcllemres  6523  tfrcldm  6524  erref  6717  1dom1el  6988  en2  6993  en2m  6994  xpdom2  7010  dom0  7019  xpen  7026  mapdom1g  7028  phplem4dom  7043  phplem4on  7049  fidceq  7051  dif1en  7061  fin0  7067  fin0or  7068  isinfinf  7079  eqsndc  7088  infm  7089  en2eqpr  7092  fiuni  7168  supelti  7192  djudom  7283  difinfsn  7290  enomnilem  7328  enmkvlem  7351  enwomnilem  7359  exmidfodomrlemim  7402  exmidaclem  7413  cc2lem  7475  cc3  7477  genpml  7727  genpmu  7728  ltexprlemm  7810  ltexprlemfl  7819  ltexprlemfu  7821  suplocsr  8019  axpre-suploc  8112  eqord1  8653  nn1suc  9152  nninfdcex  10487  zsupssdc  10488  seq3f1oleml  10768  zfz1isolem1  11094  eulerth  12795  4sqlem14  12967  4sqlem17  12970  4sqlem18  12971  ennnfonelemim  13035  exmidunben  13037  enctlem  13043  ctiunct  13051  unct  13053  omctfn  13054  omiunct  13055  relelbasov  13135  issubg2m  13766  lmff  14963  txcn  14989  suplociccreex  15338  suplociccex  15339  wlkvtxiedg  16142  wlkvtxiedgg  16143  wlkreslem  16173  3dom  16523  subctctexmid  16537  exmidsbthrlem  16562  sbthom  16566