Theorem exlimddv 1870

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

Syntax hints:   -> wi 4   /\ wa 103   E.wex 1468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie2 1470  ax-17 1506

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  fvmptdv2  5503  tfrlemi14d  6223  tfrexlem  6224  tfr1onlemres  6239  tfrcllemres  6252  tfrcldm  6253  erref  6442  xpdom2  6718  dom0  6725  xpen  6732  mapdom1g  6734  phplem4dom  6749  phplem4on  6754  fidceq  6756  dif1en  6766  fin0  6772  fin0or  6773  isinfinf  6784  infm  6791  en2eqpr  6794  fiuni  6859  supelti  6882  djudom  6971  difinfsn  6978  enomnilem  7003  exmidfodomrlemim  7050  exmidaclem  7057  genpml  7318  genpmu  7319  ltexprlemm  7401  ltexprlemfl  7410  ltexprlemfu  7412  suplocsr  7610  axpre-suploc  7703  eqord1  8238  nn1suc  8732  seq3f1oleml  10269  zfz1isolem1  10576  ennnfonelemim  11926  exmidunben  11928  enctlem  11934  ctiunct  11942  unct  11943  lmff  12407  txcn  12433  suplociccreex  12760  suplociccex  12761  subctctexmid  13185  exmidsbthrlem  13206  sbthom  13210