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-1 5  ax-2 6  ax-3 7  ax-mp 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  3831  sssn  3864  eqpw1uni  4330  nndisjeq  4429  prepeano4  4451  tfindi  4496  tfinsuc  4498  sfintfin  4532  sfinltfin  4535  vfintle  4546  vfinspsslem1  4550  nulnnn  4556  iss  5000  ovmpt4g  5710  erref  5959  erdisj  5972  enpw1  6062  enprmaplem3  6078  enprmaplem6  6081  nenpw1pwlem2  6085  ncdisjun  6136  peano4nc  6150  ncssfin  6151  nntccl  6170  ce0addcnnul  6179  ce0nnulb  6182  fce  6188  dflec3  6221  nclenc  6222  taddc  6229  addcdi  6250  dmfrec  6316  fnfreclem3  6319