Theorem exlimddv 1910

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie2 1505  ax-17 1537

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5648  tfrlemi14d  6388  tfrexlem  6389  tfr1onlemres  6404  tfrcllemres  6417  tfrcldm  6418  erref  6609  xpdom2  6887  dom0  6896  xpen  6903  mapdom1g  6905  phplem4dom  6920  phplem4on  6925  fidceq  6927  dif1en  6937  fin0  6943  fin0or  6944  isinfinf  6955  infm  6962  en2eqpr  6965  fiuni  7039  supelti  7063  djudom  7154  difinfsn  7161  enomnilem  7199  enmkvlem  7222  enwomnilem  7230  exmidfodomrlemim  7263  exmidaclem  7270  cc2lem  7328  cc3  7330  genpml  7579  genpmu  7580  ltexprlemm  7662  ltexprlemfl  7671  ltexprlemfu  7673  suplocsr  7871  axpre-suploc  7964  eqord1  8504  nn1suc  9003  seq3f1oleml  10590  zfz1isolem1  10914  nninfdcex  12093  zsupssdc  12094  eulerth  12374  4sqlem14  12545  4sqlem17  12548  4sqlem18  12549  ennnfonelemim  12584  exmidunben  12586  enctlem  12592  ctiunct  12600  unct  12602  omctfn  12603  omiunct  12604  relelbasov  12683  issubg2m  13262  lmff  14428  txcn  14454  suplociccreex  14803  suplociccex  14804  1dom1el  15553  subctctexmid  15561  exmidsbthrlem  15582  sbthom  15586