Theorem rexrot4

Description: Rotate four restricted existential quantifiers twice. (Contributed by NM, 8-Apr-2015)

	Ref	Expression
Assertion	rexrot4	$$⊢\exists x\in A\exists y\in B\exists z\in C\exists w\in D\phi \leftrightarrow \exists z\in C\exists w\in D\exists x\in A\exists y\in B\phi$$

Proof

Step	Hyp	Ref	Expression
1		rexcom13	$$⊢\exists y\in B\exists z\in C\exists w\in D\phi \leftrightarrow \exists w\in D\exists z\in C\exists y\in B\phi$$
2	1	rexbii	$$⊢\exists x\in A\exists y\in B\exists z\in C\exists w\in D\phi \leftrightarrow \exists x\in A\exists w\in D\exists z\in C\exists y\in B\phi$$
3		rexcom13	$$⊢\exists x\in A\exists w\in D\exists z\in C\exists y\in B\phi \leftrightarrow \exists z\in C\exists w\in D\exists x\in A\exists y\in B\phi$$
4	2 3	bitri	$$⊢\exists x\in A\exists y\in B\exists z\in C\exists w\in D\phi \leftrightarrow \exists z\in C\exists w\in D\exists x\in A\exists y\in B\phi$$