Theorem rexlimddv2

Description: Restricted existential elimination rule of natural deduction. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	rexlimddv2.1	$$⊢\phi \to \exists x\in A\psi$$
	rexlimddv2.2	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge \psi \right)\to \chi$$
Assertion	rexlimddv2	$$⊢\phi \to \chi$$

Proof

Step	Hyp	Ref	Expression
1		rexlimddv2.1	$$⊢\phi \to \exists x\in A\psi$$
2		rexlimddv2.2	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge \psi \right)\to \chi$$
3	2	anasss	$$⊢\left(\phi \wedge \left(x\in A\wedge \psi \right)\right)\to \chi$$
4	1 3	rexlimddv	$$⊢\phi \to \chi$$