Theorem exlimddv 1898

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie2 1494  ax-17 1526

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5605  tfrlemi14d  6333  tfrexlem  6334  tfr1onlemres  6349  tfrcllemres  6362  tfrcldm  6363  erref  6554  xpdom2  6830  dom0  6837  xpen  6844  mapdom1g  6846  phplem4dom  6861  phplem4on  6866  fidceq  6868  dif1en  6878  fin0  6884  fin0or  6885  isinfinf  6896  infm  6903  en2eqpr  6906  fiuni  6976  supelti  7000  djudom  7091  difinfsn  7098  enomnilem  7135  enmkvlem  7158  enwomnilem  7166  exmidfodomrlemim  7199  exmidaclem  7206  cc2lem  7264  cc3  7266  genpml  7515  genpmu  7516  ltexprlemm  7598  ltexprlemfl  7607  ltexprlemfu  7609  suplocsr  7807  axpre-suploc  7900  eqord1  8439  nn1suc  8937  seq3f1oleml  10502  zfz1isolem1  10819  nninfdcex  11953  zsupssdc  11954  eulerth  12232  ennnfonelemim  12424  exmidunben  12426  enctlem  12432  ctiunct  12440  unct  12442  omctfn  12443  omiunct  12444  issubg2m  13047  lmff  13685  txcn  13711  suplociccreex  14038  suplociccex  14039  subctctexmid  14686  exmidsbthrlem  14706  sbthom  14710