Theorem eximdv 1929

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

Syntax hints:   -> wi 4   E.wex 1541

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximdv  1931  reximdv2  2643  cgsexg  2851  spc3egv  2911  euind  3006  ssel  3234  reupick  3507  reximdva0m  3526  uniss  3937  eusvnfb  4577  coss1  4912  coss2  4913  ssrelrn  4949  dmss  4957  dmcosseq  5031  funssres  5397  imain  5440  brprcneu  5665  fv3  5695  dffo4  5827  dffo5  5828  f1eqcocnv  5966  mapsnd  6925  mapsn  6927  en2m  7068  ctssdccl  7404  acfun  7516  ccfunen  7580  cc4f  7585  cc4n  7587  dmaddpq  7696  dmmulpq  7697  recexprlemlol  7943  recexprlemupu  7945  ioom  10624  ctinfom  13196  ctinf  13198  omctfn  13211  nninfdclemp1  13218  ptex  13494  subgintm  13932  txcn  15157