Metamath Proof Explorer


Theorem excom13

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

Ref Expression
Assertion excom13 xyzφzyxφ

Proof

Step Hyp Ref Expression
1 excom xyzφyxzφ
2 excom xzφzxφ
3 2 exbii yxzφyzxφ
4 excom yzxφzyxφ
5 1 3 4 3bitri xyzφzyxφ