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  5795  tfrlemi14d  6604  tfrexlem  6605  tfr1onlemres  6620  tfrcllemres  6633  tfrcldm  6634  erref  6827  1dom1el  7107  en2  7112  en2m  7113  xpdom2  7129  dom0  7138  xpen  7145  mapdom1g  7147  phplem4dom  7163  phplem4on  7169  fidceq  7171  dif1en  7183  fin0  7189  fin0or  7190  isinfinf  7201  eqsndc  7210  infm  7211  en2eqpr  7214  fiuni  7312  supelti  7343  djudom  7434  difinfsn  7441  enomnilem  7479  enmkvlem  7502  enwomnilem  7510  exmidfodomrlemim  7554  exmidaclem  7565  cc2lem  7633  cc3  7635  genpml  7885  genpmu  7886  ltexprlemm  7968  ltexprlemfl  7977  ltexprlemfu  7979  suplocsr  8177  axpre-suploc  8270  eqord1  8813  nn1suc  9326  nninfdcex  10683  zsupssdc  10684  seq3f1oleml  10968  zfz1isolem1  11308  eulerth  13034  4sqlem14  13206  4sqlem17  13209  4sqlem18  13210  ennnfonelemim  13367  exmidunben  13369  enctlem  13375  ctiunct  13383  unct  13385  omctfn  13386  omiunct  13387  relelbasov  13468  issubg2m  14045  gsump1  14241  gsumf1ofi  14244  gsummhmfi  14248  gsumressfi  14251  opprringb  14470  lmff  15441  txcn  15467  suplociccreex  15816  suplociccex  15817  wlkvtxiedg  16752  wlkvtxiedgg  16753  wlkreslem  16785  eulerpathum  16888  3dom  17184  subctctexmid  17196  exmidsbthrlem  17233  sbthom  17237