Theorem exlimddv 1922

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie2 1517  ax-17 1549

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5669  tfrlemi14d  6419  tfrexlem  6420  tfr1onlemres  6435  tfrcllemres  6448  tfrcldm  6449  erref  6640  en2  6912  xpdom2  6926  dom0  6935  xpen  6942  mapdom1g  6944  phplem4dom  6959  phplem4on  6964  fidceq  6966  dif1en  6976  fin0  6982  fin0or  6983  isinfinf  6994  infm  7001  en2eqpr  7004  fiuni  7080  supelti  7104  djudom  7195  difinfsn  7202  enomnilem  7240  enmkvlem  7263  enwomnilem  7271  exmidfodomrlemim  7309  exmidaclem  7320  cc2lem  7378  cc3  7380  genpml  7630  genpmu  7631  ltexprlemm  7713  ltexprlemfl  7722  ltexprlemfu  7724  suplocsr  7922  axpre-suploc  8015  eqord1  8556  nn1suc  9055  nninfdcex  10380  zsupssdc  10381  seq3f1oleml  10661  zfz1isolem1  10985  eulerth  12555  4sqlem14  12727  4sqlem17  12730  4sqlem18  12731  ennnfonelemim  12795  exmidunben  12797  enctlem  12803  ctiunct  12811  unct  12813  omctfn  12814  omiunct  12815  relelbasov  12894  issubg2m  13525  lmff  14721  txcn  14747  suplociccreex  15096  suplociccex  15097  1dom1el  15927  subctctexmid  15937  exmidsbthrlem  15961  sbthom  15965