Theorem eximdv 1903

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

Syntax hints:   -> wi 4   E.wex 1515

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximdv  1905  reximdv2  2605  cgsexg  2807  spc3egv  2865  euind  2960  ssel  3187  reupick  3457  reximdva0m  3476  uniss  3871  eusvnfb  4502  coss1  4834  coss2  4835  dmss  4878  dmcosseq  4951  funssres  5314  imain  5357  brprcneu  5571  fv3  5601  dffo4  5730  dffo5  5731  f1eqcocnv  5862  mapsn  6779  ctssdccl  7215  acfun  7321  ccfunen  7378  cc4f  7383  cc4n  7385  dmaddpq  7494  dmmulpq  7495  recexprlemlol  7741  recexprlemupu  7743  ioom  10405  ctinfom  12832  ctinf  12834  omctfn  12847  nninfdclemp1  12854  ptex  13129  subgintm  13567  txcn  14780