Theorem excom13

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

	Ref	Expression
Assertion	excom13	|- ( E. x E. y E. z ph <-> E. z E. y E. x ph )

Proof

Step	Hyp	Ref	Expression
1		excom	|- ( E. x E. y E. z ph <-> E. y E. x E. z ph )
2		excom	|- ( E. x E. z ph <-> E. z E. x ph )
3	2	exbii	|- ( E. y E. x E. z ph <-> E. y E. z E. x ph )
4		excom	|- ( E. y E. z E. x ph <-> E. z E. y E. x ph )
5	1 3 4	3bitri	|- ( E. x E. y E. z ph <-> E. z E. y E. x ph )