Theorem eximd 1782

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypotheses

Ref	Expression
eximd.1	|- F/ x ph
eximd.2	|- ( ph -> ( ps -> ch ) )

Assertion

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

Proof of Theorem eximd

Step	Hyp	Ref	Expression
1		eximd.1	. . 3 |- F/ x ph
2	1	nfri 1774	. 2 |- ( ph -> A. x ph )
3		eximd.2	. 2 |- ( ph -> ( ps -> ch ) )
4	2, 3	eximdh 1595	1 |- ( ph -> ( E. x ps -> E. x ch ) )

Syntax hints:   -> wi 4   E.wex 1547   F/wnf 1550

This theorem is referenced by:  exlimd  1820  19.41  1896  19.41OLD  1897  exdistrf  2028  sbied  2085  mo  2276  mopick2  2321  2euex  2326  copsexg  4402  ssopab2  4440  axextnd  8422  axpowndlem3  8430  axregndlem1  8433  axregnd  8435  finminlem  26211  ssrexf  27551  stoweidlem27  27643  stoweidlem34  27650  stoweidlem35  27651  exdistrfNEW7  29211  sbiedNEW7  29244  pmapglb2xN  30254

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551