Theorem eximdv 1928

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  1930  reximdv2  2632  cgsexg  2839  spc3egv  2899  euind  2994  ssel  3222  reupick  3493  reximdva0m  3512  uniss  3919  eusvnfb  4557  coss1  4891  coss2  4892  ssrelrn  4928  dmss  4936  dmcosseq  5010  funssres  5376  imain  5419  brprcneu  5641  fv3  5671  dffo4  5803  dffo5  5804  f1eqcocnv  5942  mapsn  6902  en2m  7042  ctssdccl  7370  acfun  7482  ccfunen  7543  cc4f  7548  cc4n  7550  dmaddpq  7659  dmmulpq  7660  recexprlemlol  7906  recexprlemupu  7908  ioom  10583  ctinfom  13129  ctinf  13131  omctfn  13144  nninfdclemp1  13151  ptex  13427  subgintm  13865  txcn  15086