Theorem rexlimd2

Description: Version of rexlimd with deduction version of second hypothesis. (Contributed by NM, 21-Jul-2013) (Revised by Mario Carneiro, 8-Oct-2016)

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

Proof

Step	Hyp	Ref	Expression
1		rexlimd2.1	|- F/ x ph
2		rexlimd2.2	|- ( ph -> F/ x ch )
3		rexlimd2.3	|- ( ph -> ( x e. A -> ( ps -> ch ) ) )
4	1 3	ralrimi	|- ( ph -> A. x e. A ( ps -> ch ) )
5		r19.23t	|- ( F/ x ch -> ( A. x e. A ( ps -> ch ) <-> ( E. x e. A ps -> ch ) ) )
6	2 5	syl	|- ( ph -> ( A. x e. A ( ps -> ch ) <-> ( E. x e. A ps -> ch ) ) )
7	4 6	mpbid	|- ( ph -> ( E. x e. A ps -> ch ) )