Theorem exlimddv 1913

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie2 1508  ax-17 1540

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5654  tfrlemi14d  6400  tfrexlem  6401  tfr1onlemres  6416  tfrcllemres  6429  tfrcldm  6430  erref  6621  xpdom2  6899  dom0  6908  xpen  6915  mapdom1g  6917  phplem4dom  6932  phplem4on  6937  fidceq  6939  dif1en  6949  fin0  6955  fin0or  6956  isinfinf  6967  infm  6974  en2eqpr  6977  fiuni  7053  supelti  7077  djudom  7168  difinfsn  7175  enomnilem  7213  enmkvlem  7236  enwomnilem  7244  exmidfodomrlemim  7280  exmidaclem  7291  cc2lem  7349  cc3  7351  genpml  7601  genpmu  7602  ltexprlemm  7684  ltexprlemfl  7693  ltexprlemfu  7695  suplocsr  7893  axpre-suploc  7986  eqord1  8527  nn1suc  9026  nninfdcex  10344  zsupssdc  10345  seq3f1oleml  10625  zfz1isolem1  10949  eulerth  12426  4sqlem14  12598  4sqlem17  12601  4sqlem18  12602  ennnfonelemim  12666  exmidunben  12668  enctlem  12674  ctiunct  12682  unct  12684  omctfn  12685  omiunct  12686  relelbasov  12765  issubg2m  13395  lmff  14569  txcn  14595  suplociccreex  14944  suplociccex  14945  1dom1el  15721  subctctexmid  15731  exmidsbthrlem  15753  sbthom  15757