Metamath Proof Explorer


Theorem exrot3

Description: Rotate existential quantifiers. (Contributed by NM, 17-Mar-1995)

Ref Expression
Assertion exrot3 x y z φ y z x φ

Proof

Step Hyp Ref Expression
1 excom13 x y z φ z y x φ
2 excom z y x φ y z x φ
3 1 2 bitri x y z φ y z x φ