Good catch. I vote for removing (that is, deprecating) https://us.metamath.org/mpeuni/znnenlem.html
Benoît On Thursday, September 1, 2022 at 5:43:32 PM UTC+2 [email protected] wrote: > 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/8b88c283-92a5-4f6e-855e-50ec491a7646n%40googlegroups.com.
