Theorem exlimdh

Description: Deduction form of Theorem 19.9 of Margaris p. 89. (Contributed by NM, 28-Jan-1997)

	Ref	Expression
Hypotheses	exlimdh.1	|- ( ph -> A. x ph )
	exlimdh.2	|- ( ch -> A. x ch )
	exlimdh.3	|- ( ph -> ( ps -> ch ) )
Assertion	exlimdh	|- ( ph -> ( E. x ps -> ch ) )

Proof

Step	Hyp	Ref	Expression
1		exlimdh.1	|- ( ph -> A. x ph )
2		exlimdh.2	|- ( ch -> A. x ch )
3		exlimdh.3	|- ( ph -> ( ps -> ch ) )
4	1	nf5i	|- F/ x ph
5	2	nf5i	|- F/ x ch
6	4 5 3	exlimd	|- ( ph -> ( E. x ps -> ch ) )