Theorem rexlimd

Description: Deduction form of rexlimd . For a version based on fewer axioms see rexlimdv . (Contributed by NM, 27-May-1998) (Proof shortened by Andrew Salmon, 30-May-2011) (Proof shortened by Wolf Lammen, 14-Jan-2020)

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

Proof

Step	Hyp	Ref	Expression
1		rexlimd.1	|- F/ x ph
2		rexlimd.2	|- F/ x ch
3		rexlimd.3	|- ( ph -> ( x e. A -> ( ps -> ch ) ) )
4	2	a1i	|- ( ph -> F/ x ch )
5	1 4 3	rexlimd2	|- ( ph -> ( E. x e. A ps -> ch ) )