Metamath Proof Explorer

Theorem bj-2albi

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

Ref Expression
Assertion bj-2albi ⊢ ∀ x ∀ y φ ↔ ψ → ∀ x ∀ y φ ↔ ∀ x ∀ y ψ

Proof

Step Hyp Ref Expression
1 albi ⊢ ∀ y φ ↔ ψ → ∀ y φ ↔ ∀ y ψ
2 1 alimi ⊢ ∀ x ∀ y φ ↔ ψ → ∀ x ∀ y φ ↔ ∀ y ψ
3 albi ⊢ ∀ x ∀ y φ ↔ ∀ y ψ → ∀ x ∀ y φ ↔ ∀ x ∀ y ψ
4 2 3 syl ⊢ ∀ x ∀ y φ ↔ ψ → ∀ x ∀ y φ ↔ ∀ x ∀ y ψ