mathbox: df-bj-nnf (#3607)

Author: benjub

discouraged

@@ -17993,7 +17993,7 @@ Proof modification of "bj-denotes" is discouraged (76 steps).
 Proof modification of "bj-denotesv" is discouraged (15 steps).
 Proof modification of "bj-df-nul" is discouraged (11 steps).
 Proof modification of "bj-df-v" is discouraged (29 steps).
-Proof modification of "bj-dfnnf2" is discouraged (34 steps).
+Proof modification of "bj-dfnnf3" is discouraged (34 steps).
 Proof modification of "bj-disjsn01" is discouraged (18 steps).
 Proof modification of "bj-dral1v" is discouraged (36 steps).
 Proof modification of "bj-drex1v" is discouraged (42 steps).