Metamath Proof Explorer

Theorem bj-nfalt

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

Ref Expression
Assertion bj-nfalt ⊢ ∀ x Ⅎ y φ → Ⅎ y ∀ x φ

Proof

Step Hyp Ref Expression
1 bj-hbalt ⊢ ∀ x φ → ∀ y φ → ∀ x φ → ∀ y ∀ x φ
2 1 alimi ⊢ ∀ y ∀ x φ → ∀ y φ → ∀ y ∀ x φ → ∀ y ∀ x φ
3 2 alcoms ⊢ ∀ x ∀ y φ → ∀ y φ → ∀ y ∀ x φ → ∀ y ∀ x φ
4 nf5 ⊢ Ⅎ y φ ↔ ∀ y φ → ∀ y φ
5 4 albii ⊢ ∀ x Ⅎ y φ ↔ ∀ x ∀ y φ → ∀ y φ
6 nf5 ⊢ Ⅎ y ∀ x φ ↔ ∀ y ∀ x φ → ∀ y ∀ x φ
7 3 5 6 3imtr4i ⊢ ∀ x Ⅎ y φ → Ⅎ y ∀ x φ