Theorem eximdv 1894

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

Syntax hints:   -> wi 4   E.wex 1506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximdv  1896  reximdv2  2596  cgsexg  2798  spc3egv  2856  euind  2951  ssel  3177  reupick  3447  reximdva0m  3466  uniss  3860  eusvnfb  4489  coss1  4821  coss2  4822  dmss  4865  dmcosseq  4937  funssres  5300  imain  5340  brprcneu  5551  fv3  5581  dffo4  5710  dffo5  5711  f1eqcocnv  5838  mapsn  6749  ctssdccl  7177  acfun  7274  ccfunen  7331  cc4f  7336  cc4n  7338  dmaddpq  7446  dmmulpq  7447  recexprlemlol  7693  recexprlemupu  7695  ioom  10350  ctinfom  12645  ctinf  12647  omctfn  12660  nninfdclemp1  12667  ptex  12935  subgintm  13328  txcn  14511