Hi Alexander, I didn't move ~ ifeq123d (because it is already available as ~ ifbieq12d , > so I marked ~ ifeq123d as "discouraged") >
did you also replace all the references from ifeq123d to ifbieq12d (so that my theorems don't refer to a discouraged label, now?) Thanks Glauco -- 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/03463730-4e24-42c5-8888-f713fc191d9d%40googlegroups.com.
