Theorem eximdv 1933

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

Syntax hints:   -> wi 4   E.wex 1545

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximdv  1935  reximdv2  2649  cgsexg  2857  spc3egv  2917  euind  3013  ssel  3242  reupick  3517  reximdva0m  3537  uniss  3951  eusvnfb  4595  coss1  4930  coss2  4931  ssrelrn  4967  dmss  4975  dmcosseq  5049  funssres  5415  imain  5458  brprcneu  5683  fv3  5713  dffo4  5847  dffo5  5848  f1eqcocnv  5987  mapsnd  6960  mapsn  6962  en2m  7103  ctssdccl  7441  acfun  7553  ccfunen  7620  cc4f  7625  cc4n  7627  dmaddpq  7736  dmmulpq  7737  recexprlemlol  7983  recexprlemupu  7985  ioom  10673  ctinfom  13297  ctinf  13299  omctfn  13312  nninfdclemp1  13319  ptex  13595  subgintm  13978  txcn  15299