Theorem exlimd

Description: Deduction form of Theorem 19.9 of Margaris p. 89. (Contributed by NM, 23-Jan-1993) (Revised by Mario Carneiro, 24-Sep-2016) (Proof shortened by Wolf Lammen, 12-Jan-2018)

	Ref	Expression
Hypotheses	exlimd.1	|- F/ x ph
	exlimd.2	|- F/ x ch
	exlimd.3	|- ( ph -> ( ps -> ch ) )
Assertion	exlimd	|- ( ph -> ( E. x ps -> ch ) )

Proof

Step	Hyp	Ref	Expression
1		exlimd.1	|- F/ x ph
2		exlimd.2	|- F/ x ch
3		exlimd.3	|- ( ph -> ( ps -> ch ) )
4	1 3	eximd	|- ( ph -> ( E. x ps -> E. x ch ) )
5	2	19.9	|- ( E. x ch <-> ch )
6	4 5	syl6ib	|- ( ph -> ( E. x ps -> ch ) )