Metamath Proof Explorer


Theorem bj-nnfa1

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

Ref Expression
Assertion bj-nnfa1 Ⅎ' 𝑥𝑥 𝜑

Proof

Step Hyp Ref Expression
1 hbe1a ( ∃ 𝑥𝑥 𝜑 → ∀ 𝑥 𝜑 )
2 bj-modal4 ( ∀ 𝑥 𝜑 → ∀ 𝑥𝑥 𝜑 )
3 df-bj-nnf ( Ⅎ' 𝑥𝑥 𝜑 ↔ ( ( ∃ 𝑥𝑥 𝜑 → ∀ 𝑥 𝜑 ) ∧ ( ∀ 𝑥 𝜑 → ∀ 𝑥𝑥 𝜑 ) ) )
4 1 2 3 mpbir2an Ⅎ' 𝑥𝑥 𝜑