Theorem 19.9d2rf

Description: A deduction version of one direction of 19.9 with two variables. (Contributed by Thierry Arnoux, 20-Mar-2017)

	Ref	Expression
Hypotheses	19.9d2rf.0	$$⊢Ⅎy\phi$$
	19.9d2rf.1	$$⊢\phi \to Ⅎx\psi$$
	19.9d2rf.2	$$⊢\phi \to Ⅎy\psi$$
	19.9d2rf.3	$$⊢\phi \to \exists x\in A\exists y\in B\psi$$
Assertion	19.9d2rf	$$⊢\phi \to \psi$$

Proof

Step	Hyp	Ref	Expression
1		19.9d2rf.0	$$⊢Ⅎy\phi$$
2		19.9d2rf.1	$$⊢\phi \to Ⅎx\psi$$
3		19.9d2rf.2	$$⊢\phi \to Ⅎy\psi$$
4		19.9d2rf.3	$$⊢\phi \to \exists x\in A\exists y\in B\psi$$
5		rexex	$$⊢\exists x\in A\exists y\in B\psi \to \exists x\exists y\in B\psi$$
6		rexex	$$⊢\exists y\in B\psi \to \exists y\psi$$
7	6	eximi	$$⊢\exists x\exists y\in B\psi \to \exists x\exists y\psi$$
8	4 5 7	3syl	$$⊢\phi \to \exists x\exists y\psi$$
9	1 2	nfexd	$$⊢\phi \to Ⅎx\exists y\psi$$
10	9	19.9d	$$⊢\phi \to \left(\exists x\exists y\psi \to \exists y\psi \right)$$
11	8 10	mpd	$$⊢\phi \to \exists y\psi$$
12	3	19.9d	$$⊢\phi \to \left(\exists y\psi \to \psi \right)$$
13	11 12	mpd	$$⊢\phi \to \psi$$