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  2836  spc3egv  2896  euind  2991  ssel  3219  reupick  3489  reximdva0m  3508  uniss  3910  eusvnfb  4547  coss1  4881  coss2  4882  ssrelrn  4918  dmss  4926  dmcosseq  5000  funssres  5364  imain  5407  brprcneu  5626  fv3  5656  dffo4  5789  dffo5  5790  f1eqcocnv  5925  mapsn  6852  en2m  6992  ctssdccl  7299  acfun  7410  ccfunen  7471  cc4f  7476  cc4n  7478  dmaddpq  7587  dmmulpq  7588  recexprlemlol  7834  recexprlemupu  7836  ioom  10508  ctinfom  13036  ctinf  13038  omctfn  13051  nninfdclemp1  13058  ptex  13334  subgintm  13772  txcn  14986