Theorem eximdv 1860

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)

Hypothesis

Ref	Expression
alimdv.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
eximdv	|- ( ph -> ( E. x ps -> E. x ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)

Proof of Theorem eximdv

Step	Hyp	Ref	Expression
1		ax-17 1506	. 2 |- ( ph -> A. x ph )
2		alimdv.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	eximdh 1591	1 |- ( ph -> ( E. x ps -> E. x ch ) )

Syntax hints:   -> wi 4   E.wex 1472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2eximdv  1862  reximdv2  2556  cgsexg  2747  spc3egv  2804  euind  2899  ssel  3122  reupick  3391  reximdva0m  3409  uniss  3794  eusvnfb  4415  coss1  4742  coss2  4743  dmss  4786  dmcosseq  4858  funssres  5213  imain  5253  brprcneu  5462  fv3  5492  dffo4  5616  dffo5  5617  f1eqcocnv  5742  mapsn  6636  ctssdccl  7056  acfun  7143  ccfunen  7185  cc4f  7190  cc4n  7192  dmaddpq  7300  dmmulpq  7301  recexprlemlol  7547  recexprlemupu  7549  ioom  10164  ctinfom  12199  ctinf  12201  omctfn  12214  nninfdclemp1  12223  txcn  12717