Metamath Proof Explorer

Theorem bj-3exbi

Description: Closed form of 3exbii . (Contributed by BJ, 6-May-2019)

Ref Expression
Assertion bj-3exbi ⊢ ∀ x ∀ y ∀ z φ ↔ ψ → ∃ x ∃ y ∃ z φ ↔ ∃ x ∃ y ∃ z ψ

Proof

Step Hyp Ref Expression
1 exbi ⊢ ∀ z φ ↔ ψ → ∃ z φ ↔ ∃ z ψ
2 1 2alimi ⊢ ∀ x ∀ y ∀ z φ ↔ ψ → ∀ x ∀ y ∃ z φ ↔ ∃ z ψ
3 bj-2exbi ⊢ ∀ x ∀ y ∃ z φ ↔ ∃ z ψ → ∃ x ∃ y ∃ z φ ↔ ∃ x ∃ y ∃ z ψ
4 2 3 syl ⊢ ∀ x ∀ y ∀ z φ ↔ ψ → ∃ x ∃ y ∃ z φ ↔ ∃ x ∃ y ∃ z ψ