Theorem exlimddv 1923

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie2 1518  ax-17 1550

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5692  tfrlemi14d  6442  tfrexlem  6443  tfr1onlemres  6458  tfrcllemres  6471  tfrcldm  6472  erref  6663  en2  6936  en2m  6937  xpdom2  6951  dom0  6960  xpen  6967  mapdom1g  6969  phplem4dom  6984  phplem4on  6990  fidceq  6992  dif1en  7002  fin0  7008  fin0or  7009  isinfinf  7020  infm  7027  en2eqpr  7030  fiuni  7106  supelti  7130  djudom  7221  difinfsn  7228  enomnilem  7266  enmkvlem  7289  enwomnilem  7297  exmidfodomrlemim  7340  exmidaclem  7351  cc2lem  7413  cc3  7415  genpml  7665  genpmu  7666  ltexprlemm  7748  ltexprlemfl  7757  ltexprlemfu  7759  suplocsr  7957  axpre-suploc  8050  eqord1  8591  nn1suc  9090  nninfdcex  10417  zsupssdc  10418  seq3f1oleml  10698  zfz1isolem1  11022  eulerth  12670  4sqlem14  12842  4sqlem17  12845  4sqlem18  12846  ennnfonelemim  12910  exmidunben  12912  enctlem  12918  ctiunct  12926  unct  12928  omctfn  12929  omiunct  12930  relelbasov  13009  issubg2m  13640  lmff  14836  txcn  14862  suplociccreex  15211  suplociccex  15212  1dom1el  16126  subctctexmid  16139  exmidsbthrlem  16163  sbthom  16167