Description: Nonfreeness in the antecedent and the consequent of an implication implies nonfreeness in the implication. (Contributed by BJ, 27-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-nnfim |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.35 | ||
2 | bj-nnfim2 | ||
3 | 1 2 | syl5bi | |
4 | bj-nnfim1 | ||
5 | 19.38 | ||
6 | 4 5 | syl6 | |
7 | df-bj-nnf | ||
8 | 3 6 7 | sylanbrc |