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

Metamath Proof Explorer

Theorem bj-nnfa1

Description: See nfa1 . (Contributed by BJ, 12-Aug-2023) (Proof modification is discouraged.)

Ref Expression
Assertion bj-nnfa1 ⊢ Ⅎ' x ∀ x φ

Proof

Step Hyp Ref Expression
1 hbe1a ⊢ ∃ x ∀ x φ → ∀ x φ
2 bj-modal4 ⊢ ∀ x φ → ∀ x ∀ x φ
3 df-bj-nnf ⊢ Ⅎ' x ∀ x φ ↔ ∃ x ∀ x φ → ∀ x φ ∧ ∀ x φ → ∀ x ∀ x φ
4 1 2 3 mpbir2an ⊢ Ⅎ' x ∀ x φ