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  2853  euind  2948  ssel  3174  reupick  3444  reximdva0m  3463  uniss  3857  eusvnfb  4486  coss1  4818  coss2  4819  dmss  4862  dmcosseq  4934  funssres  5297  imain  5337  brprcneu  5548  fv3  5578  dffo4  5707  dffo5  5708  f1eqcocnv  5835  mapsn  6746  ctssdccl  7172  acfun  7269  ccfunen  7326  cc4f  7331  cc4n  7333  dmaddpq  7441  dmmulpq  7442  recexprlemlol  7688  recexprlemupu  7690  ioom  10332  ctinfom  12588  ctinf  12590  omctfn  12603  nninfdclemp1  12610  ptex  12878  subgintm  13271  txcn  14454