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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-nnfea | ||
2 | bj-19.21bit | ||
3 | bj-19.23bit | ||
4 | df-bj-nnf | ||
5 | 2 3 4 | sylanbrc | |
6 | 1 5 | impbii |