Theorem eximd 1750

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 1742	. 2 |- ( ph -> A. x ph )
3		eximd.2	. 2 |- ( ph -> ( ps -> ch ) )
4	2, 3	eximdh 1575	1 |- ( ph -> ( E. x ps -> E. x ch ) )

Syntax hints:   -> wi 4   E.wex 1528   F/wnf 1531

This theorem is referenced by:  19.41  1815  exdistrf  1911  sbied  1976  mo  2165  mopick2  2210  2euex  2215  copsexg  4252  ssopab2  4290  axextnd  8213  axpowndlem3  8221  axregndlem1  8224  axregnd  8226  ishashinf  23389  finminlem  26231  ssrexf  27684  stoweidlem27  27776  stoweidlem34  27783  stoweidlem35  27784  pmapglb2xN  29961

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715

This theorem depends on definitions:  df-bi 177  df-ex 1529  df-nf 1532