Metamath Proof Explorer


Theorem bj-nnfe1

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

Ref Expression
Assertion bj-nnfe1
|- F// x E. x ph

Proof

Step Hyp Ref Expression
1 bj-modal4e
 |-  ( E. x E. x ph -> E. x ph )
2 hbe1
 |-  ( E. x ph -> A. x E. x ph )
3 df-bj-nnf
 |-  ( F// x E. x ph <-> ( ( E. x E. x ph -> E. x ph ) /\ ( E. x ph -> A. x E. x ph ) ) )
4 1 2 3 mpbir2an
 |-  F// x E. x ph