Hi Glauco, no, I did not replace ifeq123d by ifbieq12d in any proof. Since the theorems are not identical (they use different class variables), this is not possible by a simple find&replace. But there is no urgency to replace ifeq123d by ifbieq12d although ifeq123d is discouraged - the proofs using ifeq123d are still valid. I marked feq123d as "discouraged" so that it will/should not be used in additional proofs.
Alexander On Saturday, December 21, 2019 at 10:42:41 PM UTC+1, Glauco wrote: > > 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/e67dbda5-c7a2-400e-9cdd-41edc7b0eb75%40googlegroups.com.
