This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bj-nnfalt

Description: See nfal and bj-nfalt . (Contributed by BJ, 12-Aug-2023) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 df-bj-nnf ⊢ Ⅎ' y φ ↔ ∃ y φ → φ ∧ φ → ∀ y φ
2 1 albii ⊢ ∀ x Ⅎ' y φ ↔ ∀ x ∃ y φ → φ ∧ φ → ∀ y φ
3 simpl ⊢ ∃ y φ → φ ∧ φ → ∀ y φ → ∃ y φ → φ
4 3 alimi ⊢ ∀ x ∃ y φ → φ ∧ φ → ∀ y φ → ∀ x ∃ y φ → φ
5 bj-nnflemea ⊢ ∀ x ∃ y φ → φ → ∃ y ∀ x φ → ∀ x φ
6 4 5 syl ⊢ ∀ x ∃ y φ → φ ∧ φ → ∀ y φ → ∃ y ∀ x φ → ∀ x φ
7 2 6 sylbi ⊢ ∀ x Ⅎ' y φ → ∃ y ∀ x φ → ∀ x φ
8 simpr ⊢ ∃ y φ → φ ∧ φ → ∀ y φ → φ → ∀ y φ
9 8 alimi ⊢ ∀ x ∃ y φ → φ ∧ φ → ∀ y φ → ∀ x φ → ∀ y φ
10 bj-nnflemaa ⊢ ∀ x φ → ∀ y φ → ∀ x φ → ∀ y ∀ x φ
11 9 10 syl ⊢ ∀ x ∃ y φ → φ ∧ φ → ∀ y φ → ∀ x φ → ∀ y ∀ x φ
12 2 11 sylbi ⊢ ∀ x Ⅎ' y φ → ∀ x φ → ∀ y ∀ x φ
13 df-bj-nnf ⊢ Ⅎ' y ∀ x φ ↔ ∃ y ∀ x φ → ∀ x φ ∧ ∀ x φ → ∀ y ∀ x φ
14 7 12 13 sylanbrc ⊢ ∀ x Ⅎ' y φ → Ⅎ' y ∀ x φ