Znnenlem?

[David Starner]

Should znnenlem be removed from set.mm or moved to a mathbox? It claims to be a lemma for znnen, but it's no longer used, and while lines 16 and 28 prove moderately interesting things, it then turns A -> B and C -> D into (A /\ B) -> (C <-> D). So maybe splittable into three theorems?

[Benoit]

Good catch.  I vote for removing (that is, deprecating) https://us.metamath.org/mpeuni/znnenlem.html

Benoît

[Alexander van der Vekens]

It is really a strange theorem: both sides of the biconditional are wrong ( x=y is wrong, because 0 <_ x and y < 0; and 2x = -2y+1would mean that an even number is equal to an odd number.

Therefore, this theorem can be deprecated and removed later.

[Benoit]

Deprecated in https://github.com/metamath/set.mm/pull/2816

Benoît