Theorem exlimddv 1891

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

Syntax hints:   -> wi 4   /\ wa 103   E.wex 1485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie2 1487  ax-17 1519

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  fvmptdv2  5585  tfrlemi14d  6312  tfrexlem  6313  tfr1onlemres  6328  tfrcllemres  6341  tfrcldm  6342  erref  6533  xpdom2  6809  dom0  6816  xpen  6823  mapdom1g  6825  phplem4dom  6840  phplem4on  6845  fidceq  6847  dif1en  6857  fin0  6863  fin0or  6864  isinfinf  6875  infm  6882  en2eqpr  6885  fiuni  6955  supelti  6979  djudom  7070  difinfsn  7077  enomnilem  7114  enmkvlem  7137  enwomnilem  7145  exmidfodomrlemim  7178  exmidaclem  7185  cc2lem  7228  cc3  7230  genpml  7479  genpmu  7480  ltexprlemm  7562  ltexprlemfl  7571  ltexprlemfu  7573  suplocsr  7771  axpre-suploc  7864  eqord1  8402  nn1suc  8897  seq3f1oleml  10459  zfz1isolem1  10775  nninfdcex  11908  zsupssdc  11909  eulerth  12187  ennnfonelemim  12379  exmidunben  12381  enctlem  12387  ctiunct  12395  unct  12397  omctfn  12398  omiunct  12399  lmff  13043  txcn  13069  suplociccreex  13396  suplociccex  13397  subctctexmid  14034  exmidsbthrlem  14054  sbthom  14058