Theorem eximdv 1873

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

Syntax hints:   -> wi 4   E.wex 1485

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2eximdv  1875  reximdv2  2569  cgsexg  2765  spc3egv  2822  euind  2917  ssel  3141  reupick  3411  reximdva0m  3430  uniss  3817  eusvnfb  4439  coss1  4766  coss2  4767  dmss  4810  dmcosseq  4882  funssres  5240  imain  5280  brprcneu  5489  fv3  5519  dffo4  5644  dffo5  5645  f1eqcocnv  5770  mapsn  6668  ctssdccl  7088  acfun  7184  ccfunen  7226  cc4f  7231  cc4n  7233  dmaddpq  7341  dmmulpq  7342  recexprlemlol  7588  recexprlemupu  7590  ioom  10217  ctinfom  12383  ctinf  12385  omctfn  12398  nninfdclemp1  12405  txcn  13069