Metamath Proof Explorer


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 )