Theorem exlimddv 1954

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie2 1547  ax-17 1579

This proof depends on definitions:  df-bi 117

This theorem is used by:  fvmptdv2  5798  tfrlemi14d  6609  tfrexlem  6610  tfr1onlemres  6625  tfrcllemres  6638  tfrcldm  6639  erref  6832  1dom1el  7113  en2  7118  en2m  7119  xpdom2  7135  dom0  7144  xpen  7151  mapdom1g  7153  phplem4dom  7169  phplem4on  7175  fidceq  7177  dif1en  7189  fin0  7195  fin0or  7196  isinfinf  7207  eqsndc  7216  infm  7217  en2eqpr  7220  funisfsuppdc  7298  fiuni  7317  supelti  7348  djudom  7439  difinfsn  7446  enomnilem  7484  enmkvlem  7507  enwomnilem  7515  exmidfodomrlemim  7559  exmidaclem  7570  cc2lem  7638  cc3  7640  genpml  7890  genpmu  7891  ltexprlemm  7973  ltexprlemfl  7982  ltexprlemfu  7984  suplocsr  8182  axpre-suploc  8275  eqord1  8818  nn1suc  9332  nninfdcex  10688  zsupssdc  10689  seq3f1oleml  10973  zfz1isolem1  11313  eulerth  13039  4sqlem14  13211  4sqlem17  13214  4sqlem18  13215  ennnfonelemim  13372  exmidunben  13374  enctlem  13380  ctiunct  13388  unct  13390  omctfn  13391  omiunct  13392  relelbasov  13473  issubg2m  14050  gsump1  14246  gsumf1ofi  14249  gsummhmfi  14263  gsumressfi  14266  opprringb  14494  psrbagmax  15183  mplsubgfilemcl  15232  mplsubgfileminv  15233  lmff  15492  txcn  15518  suplociccreex  15867  suplociccex  15868  wlkvtxiedg  16808  wlkvtxiedgg  16809  wlkreslem  16841  eulerpathum  16944  3dom  17240  subctctexmid  17252  exmidsbthrlem  17290  sbthom  17294