Theorem eximdv 1852

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 1590	1 |- ( ph -> ( E. x ps -> E. x ch ) )

Syntax hints:   -> wi 4   E.wex 1468

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2eximdv  1854  reximdv2  2529  cgsexg  2716  spc3egv  2772  euind  2866  ssel  3086  reupick  3355  reximdva0m  3373  uniss  3752  eusvnfb  4370  coss1  4689  coss2  4690  dmss  4733  dmcosseq  4805  funssres  5160  imain  5200  brprcneu  5407  fv3  5437  dffo4  5561  dffo5  5562  f1eqcocnv  5685  mapsn  6577  ctssdccl  6989  acfun  7056  ccfunen  7072  dmaddpq  7180  dmmulpq  7181  recexprlemlol  7427  recexprlemupu  7429  ioom  10031  ctinfom  11930  ctinf  11932  txcn  12433