Theorem exlimdv 1742

Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)

Hypothesis

Ref	Expression
exlimdv.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
exlimdv	|- ( ph -> ( E. x ps -> ch ) )

Distinct variable groups:   ch, x   ph, x

Allowed substitution hint:   ps( x)

Proof of Theorem exlimdv

Step	Hyp	Ref	Expression
1		ax-17 1460	. 2 |- ( ph -> A. x ph )
2		ax-17 1460	. 2 |- ( ch -> A. x ch )
3		exlimdv.1	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 2, 3	exlimdh 1528	1 |- ( ph -> ( E. x ps -> ch ) )

Syntax hints:   -> wi 4   E.wex 1422

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-5 1377  ax-gen 1379  ax-ie2 1424  ax-17 1460

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  ax11v2  1743  exlimdvv  1820  exlimddv  1821  tpid3g  3523  sssnm  3566  euotd  4037  ralxfr2d  4242  rexxfr2d  4243  releldmb  4619  relelrnb  4620  elres  4694  iss  4704  imain  5032  elunirn  5457  ovmpt4g  5674  op1steq  5856  fo2ndf  5899  reldmtpos  5922  rntpos  5926  tfrlemibacc  5995  tfrlemibxssdm  5996  tfrlemibfn  5997  tfrexlem  6003  tfr1onlembacc  6011  tfr1onlembxssdm  6012  tfr1onlembfn  6013  tfrcllembacc  6024  tfrcllembxssdm  6025  tfrcllembfn  6026  xpdom3m  6399  phplem4  6411  phpm  6421  findcard2  6445  findcard2s  6446  ac6sfi  6454  xpfi  6472  ordiso  6541  pm54.43  6570  recclnq  6696  ltexnqq  6712  ltbtwnnqq  6719  recexprlemss1l  6939  recexprlemss1u  6940  negm  8833  ioom  9399  fiinfnf1o  9862  fihashf1rn  9865  climcau  10385