Metamath Proof Explorer


Theorem excom13

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

Ref Expression
Assertion excom13 ( ∃ 𝑥𝑦𝑧 𝜑 ↔ ∃ 𝑧𝑦𝑥 𝜑 )

Proof

Step Hyp Ref Expression
1 excom ( ∃ 𝑥𝑦𝑧 𝜑 ↔ ∃ 𝑦𝑥𝑧 𝜑 )
2 excom ( ∃ 𝑥𝑧 𝜑 ↔ ∃ 𝑧𝑥 𝜑 )
3 2 exbii ( ∃ 𝑦𝑥𝑧 𝜑 ↔ ∃ 𝑦𝑧𝑥 𝜑 )
4 excom ( ∃ 𝑦𝑧𝑥 𝜑 ↔ ∃ 𝑧𝑦𝑥 𝜑 )
5 1 3 4 3bitri ( ∃ 𝑥𝑦𝑧 𝜑 ↔ ∃ 𝑧𝑦𝑥 𝜑 )