Metamath Proof Explorer

Theorem pm11.6

Description: Theorem *11.6 in WhiteheadRussell p. 165. (Contributed by Andrew Salmon, 25-May-2011)

Ref Expression
Assertion pm11.6 ⊢ ∃ x ∃ y φ ∧ ψ ∧ χ ↔ ∃ y ∃ x φ ∧ χ ∧ ψ

Proof

Step Hyp Ref Expression
1 excom ⊢ ∃ x ∃ y φ ∧ ψ ∧ χ ↔ ∃ y ∃ x φ ∧ ψ ∧ χ
2 an32 ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ χ ∧ ψ
3 2 2exbii ⊢ ∃ y ∃ x φ ∧ ψ ∧ χ ↔ ∃ y ∃ x φ ∧ χ ∧ ψ
4 1 3 bitri ⊢ ∃ x ∃ y φ ∧ ψ ∧ χ ↔ ∃ y ∃ x φ ∧ χ ∧ ψ
5 19.41v ⊢ ∃ y φ ∧ ψ ∧ χ ↔ ∃ y φ ∧ ψ ∧ χ
6 5 exbii ⊢ ∃ x ∃ y φ ∧ ψ ∧ χ ↔ ∃ x ∃ y φ ∧ ψ ∧ χ
7 19.41v ⊢ ∃ x φ ∧ χ ∧ ψ ↔ ∃ x φ ∧ χ ∧ ψ
8 7 exbii ⊢ ∃ y ∃ x φ ∧ χ ∧ ψ ↔ ∃ y ∃ x φ ∧ χ ∧ ψ
9 4 6 8 3bitr3i ⊢ ∃ x ∃ y φ ∧ ψ ∧ χ ↔ ∃ y ∃ x φ ∧ χ ∧ ψ