Theorem eximdv 1891

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

Syntax hints:   -> wi 4   E.wex 1503

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximdv  1893  reximdv2  2593  cgsexg  2795  spc3egv  2852  euind  2947  ssel  3173  reupick  3443  reximdva0m  3462  uniss  3856  eusvnfb  4485  coss1  4817  coss2  4818  dmss  4861  dmcosseq  4933  funssres  5296  imain  5336  brprcneu  5547  fv3  5577  dffo4  5706  dffo5  5707  f1eqcocnv  5834  mapsn  6744  ctssdccl  7170  acfun  7267  ccfunen  7324  cc4f  7329  cc4n  7331  dmaddpq  7439  dmmulpq  7440  recexprlemlol  7686  recexprlemupu  7688  ioom  10329  ctinfom  12585  ctinf  12587  omctfn  12600  nninfdclemp1  12607  ptex  12875  subgintm  13268  txcn  14443