Theorem exlimdv 1700

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 1419	. 2 |- ( ph -> A. x ph )
2		ax-17 1419	. 2 |- ( ch -> A. x ch )
3		exlimdv.1	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 2, 3	exlimdh 1487	1 |- ( ph -> ( E. x ps -> ch ) )

Syntax hints:   -> wi 4   E.wex 1381

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-5 1336  ax-gen 1338  ax-ie2 1383  ax-17 1419

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  ax11v2  1701  exlimdvv  1777  exlimddv  1778  tpid3g  3483  sssnm  3525  euotd  3991  ralxfr2d  4196  rexxfr2d  4197  releldmb  4571  relelrnb  4572  elres  4646  iss  4654  imain  4981  elunirn  5405  ovmpt4g  5623  op1steq  5805  fo2ndf  5848  reldmtpos  5868  rntpos  5872  tfrlemibacc  5940  tfrlemibxssdm  5941  tfrlemibfn  5942  tfrexlem  5948  freccl  5993  xpdom3m  6308  phplem4  6318  phpm  6327  findcard2  6346  findcard2s  6347  ac6sfi  6352  ordiso  6358  recclnq  6490  ltexnqq  6506  ltbtwnnqq  6513  recexprlemss1l  6733  recexprlemss1u  6734  negm  8550  climcau  9866