excom13

Description: Swap 1st and 3rd existential quantifiers. (Contributed by NM, 9-Mar-1995)

		Ref	Expression
	Assertion	excom13	$⊢ \exists x \exists y \exists z φ \leftrightarrow \exists z \exists y \exists x φ$

Step	Hyp	Ref	Expression
1		excom	$⊢ \exists x \exists y \exists z φ \leftrightarrow \exists y \exists x \exists z φ$
2		excom	$⊢ \exists x \exists z φ \leftrightarrow \exists z \exists x φ$
3	2	exbii	$⊢ \exists y \exists x \exists z φ \leftrightarrow \exists y \exists z \exists x φ$
4		excom	$⊢ \exists y \exists z \exists x φ \leftrightarrow \exists z \exists y \exists x φ$
5	1 3 4	3bitri	$⊢ \exists x \exists y \exists z φ \leftrightarrow \exists z \exists y \exists x φ$

Metamath Proof Explorer