Metamath Proof Explorer


Theorem bj-dfnnf3

Description: Alternate definition of nonfreeness when sp is available. (Contributed by BJ, 28-Jul-2023) The proof should not rely on df-nf . (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 bj-nnfea Ⅎ' x φ x φ x φ
2 bj-19.21bit x φ x φ x φ φ
3 bj-19.23bit x φ x φ φ x φ
4 df-bj-nnf Ⅎ' x φ x φ φ φ x φ
5 2 3 4 sylanbrc x φ x φ Ⅎ' x φ
6 1 5 impbii Ⅎ' x φ x φ x φ