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?
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAMZ%3Dzj4kvWY_qj-r0a99UUrvi2ZGH8_yfjifXkSKe265JooFnw%40mail.gmail.com.
