Metamath Proof Explorer


Theorem bj-nnfe

Description: Nonfreeness implies the equivalent of ax5e . (Contributed by BJ, 28-Jul-2023)

Ref Expression
Assertion bj-nnfe Ⅎ' x φ x φ φ

Proof

Step Hyp Ref Expression
1 df-bj-nnf Ⅎ' x φ x φ φ φ x φ
2 1 simplbi Ⅎ' x φ x φ φ