Theorem rexlim2d

Description: Inference removing two restricted quantifiers. Same as rexlimdvv , but with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	rexlim2d.x	$$⊢Ⅎx\phi$$
	rexlim2d.y	$$⊢Ⅎy\phi$$
	rexlim2d.3	$$⊢\phi \to \left(\left(x\in A\wedge y\in B\right)\to \left(\psi \to \chi \right)\right)$$
Assertion	rexlim2d	$$⊢\phi \to \left(\exists x\in A\exists y\in B\psi \to \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		rexlim2d.x	$$⊢Ⅎx\phi$$
2		rexlim2d.y	$$⊢Ⅎy\phi$$
3		rexlim2d.3	$$⊢\phi \to \left(\left(x\in A\wedge y\in B\right)\to \left(\psi \to \chi \right)\right)$$
4		nfv	$$⊢Ⅎx\chi$$
5		nfv	$$⊢Ⅎyx\in A$$
6	2 5	nfan	$$⊢Ⅎy\left(\phi \wedge x\in A\right)$$
7		nfv	$$⊢Ⅎy\chi$$
8	3	expdimp	$$⊢\left(\phi \wedge x\in A\right)\to \left(y\in B\to \left(\psi \to \chi \right)\right)$$
9	6 7 8	rexlimd	$$⊢\left(\phi \wedge x\in A\right)\to \left(\exists y\in B\psi \to \chi \right)$$
10	9	ex	$$⊢\phi \to \left(x\in A\to \left(\exists y\in B\psi \to \chi \right)\right)$$
11	1 4 10	rexlimd	$$⊢\phi \to \left(\exists x\in A\exists y\in B\psi \to \chi \right)$$