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	$$⊢Ⅎx\phi$$
	rexlimd.2	$$⊢Ⅎx\chi$$
	rexlimd.3	$$⊢\phi \to \left(x\in A\to \left(\psi \to \chi \right)\right)$$
Assertion	rexlimd	$$⊢\phi \to \left(\exists x\in A\psi \to \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		rexlimd.1	$$⊢Ⅎx\phi$$
2		rexlimd.2	$$⊢Ⅎx\chi$$
3		rexlimd.3	$$⊢\phi \to \left(x\in A\to \left(\psi \to \chi \right)\right)$$
4	2	a1i	$$⊢\phi \to Ⅎx\chi$$
5	1 4 3	rexlimd2	$$⊢\phi \to \left(\exists x\in A\psi \to \chi \right)$$