Theorem eximdv 1802

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 1460	. 2 |- ( ph -> A. x ph )
2		alimdv.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	eximdh 1543	1 |- ( ph -> ( E. x ps -> E. x ch ) )

Syntax hints:   -> wi 4   E.wex 1422

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  2eximdv  1804  reximdv2  2461  cgsexg  2635  spc3egv  2690  euind  2780  ssel  2994  reupick  3255  reximdva0m  3270  uniss  3630  eusvnfb  4212  coss1  4519  coss2  4520  dmss  4562  dmcosseq  4631  funssres  4972  imain  5012  brprcneu  5202  fv3  5229  dffo4  5347  dffo5  5348  f1eqcocnv  5462  dmaddpq  6631  dmmulpq  6632  recexprlemlol  6878  recexprlemupu  6880  ioom  9347