Metamath Proof Explorer


Theorem bj-nnfe1

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

Ref Expression
Assertion bj-nnfe1 Ⅎ' x x φ

Proof

Step Hyp Ref Expression
1 bj-modal4e x x φ x φ
2 hbe1 x φ x x φ
3 df-bj-nnf Ⅎ' x x φ x x φ x φ x φ x x φ
4 1 2 3 mpbir2an Ⅎ' x x φ