Theorem eximdv 1926

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

Syntax hints:   -> wi 4   E.wex 1538

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximdv  1928  reximdv2  2629  cgsexg  2835  spc3egv  2895  euind  2990  ssel  3218  reupick  3488  reximdva0m  3507  uniss  3909  eusvnfb  4545  coss1  4877  coss2  4878  ssrelrn  4914  dmss  4922  dmcosseq  4996  funssres  5360  imain  5403  brprcneu  5620  fv3  5650  dffo4  5783  dffo5  5784  f1eqcocnv  5915  mapsn  6837  en2m  6974  ctssdccl  7278  acfun  7389  ccfunen  7450  cc4f  7455  cc4n  7457  dmaddpq  7566  dmmulpq  7567  recexprlemlol  7813  recexprlemupu  7815  ioom  10480  ctinfom  12999  ctinf  13001  omctfn  13014  nninfdclemp1  13021  ptex  13297  subgintm  13735  txcn  14949