Theorem exlimdv 1636

Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.) (Revised by Wolf Lammen to remove dependency on ax-9 and ax-8, 4-Dec-2017.)

Hypothesis

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

Assertion

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

Distinct variable groups:   ch,x   ph,x

Allowed substitution hint:   ps(x)

Proof of Theorem exlimdv

Step	Hyp	Ref	Expression
1		exlimdv.1	. . 3 |- (ph -> (ps -> ch))
2	1	eximdv 1622	. 2 |- (ph -> (E.xps -> E.xch))
3		ax17e 1618	. 2 |- (E.xch -> ch)
4	2, 3	syl6 29	1 |- (ph -> (E.xps -> ch))

Syntax hints:   -> wi 4  E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  exlimdvv  1637  exlimddv  1638  ax10  1944  ax11v2  1992  ax11eq  2193  ax11el  2194  ax11inda  2200  ax11v2-o  2201  tpid3g  3832  sssn  3865  eqpw1uni  4331  nndisjeq  4430  prepeano4  4452  tfindi  4497  tfinsuc  4499  sfintfin  4533  sfinltfin  4536  vfintle  4547  vfinspsslem1  4551  nulnnn  4557  iss  5001  ovmpt4g  5711  erref  5960  erdisj  5973  enpw1  6063  enprmaplem3  6079  enprmaplem6  6082  nenpw1pwlem2  6086  ncdisjun  6137  peano4nc  6151  ncssfin  6152  nntccl  6171  ce0addcnnul  6180  ce0nnulb  6183  fce  6189  dflec3  6222  nclenc  6223  taddc  6230  addcdi  6251  dmfrec  6317  fnfreclem3  6320