Theorem eximdv 1880

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

Syntax hints:   -> wi 4   E.wex 1492

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximdv  1882  reximdv2  2576  cgsexg  2772  spc3egv  2829  euind  2924  ssel  3149  reupick  3419  reximdva0m  3438  uniss  3830  eusvnfb  4453  coss1  4781  coss2  4782  dmss  4825  dmcosseq  4897  funssres  5257  imain  5297  brprcneu  5507  fv3  5537  dffo4  5663  dffo5  5664  f1eqcocnv  5789  mapsn  6687  ctssdccl  7107  acfun  7203  ccfunen  7260  cc4f  7265  cc4n  7267  dmaddpq  7375  dmmulpq  7376  recexprlemlol  7622  recexprlemupu  7624  ioom  10256  ctinfom  12421  ctinf  12423  omctfn  12436  nninfdclemp1  12443  subgintm  12989  txcn  13646