eqab -> eqabb

[wlammen]

Follow up of #4673 .

1. eqab is renamed to eqabb;
2. eqabc is renamed to eqabbc;
3. eqabw is renamed to eqabbw. These changes were suggested in Consistent naming #4659 ;
4. update nf.mm to my latest name changes, and flip the sides of abbib there, too;
5. update mmset.raw.html;
6. shorten eqabr, no OLD version, because it was introduced by me just a few days ago;
7. delete outdated OLD theorem.

Since eqab and eqabw are intermediate names created on 15-Feb-25, I reused the lines in changes-set.txt, instead of creating new ones at the top.

I noted that in nf.mm still the old names of bitrid (syl5ib and so on) are in use.

Before continuing with the next theorem eqabc in the next pull request, I'd like to hear whether eqabcb or eqabbc is the preferred new name. I lean towards the second one (eqabbc is picked).

[icecream17]

After thinking about it, I can see the idea it might make more sense to avoid "c" being interpreted as commuting the whole biconditional (instead of both sides of the biconditional). The meaning of "c" in eqabc conflicts with that usual interpretation, however.

So eqabbc is a little more elegant, but eqabcb is slightly less ambiguous. Empirical evidence shows that when I have an initial impression but find countering evidence, I usually should've changed my mind a bit faster, so a very weak preference for eqabcb.

Other than this potential change, approve

[wlammen]

sylancb is an example of where a c is used as a suffix, but not in the meaning of "commutation" but "contraction" instead. So the "cb" ending is also ambiguous. I came across this example while investigating the usage of suffixes. biimprcd is an example where the c is placed before the final d. This is explicable, since "Deduction" is the overall outer form of this theorem, while the c is tied to some inner process. The same holds for the r suffix, so this supports in a way your view. On the other hand it is more difficult to guess the ground form from eqabcb (unlike biimprcd, sylancb). So there is more to say, on top of your findings.

I'll leave this PR open until, say, tomorrow, so if there is a majority for eqabcb, then I will adopt this solution. This, of course, does not finalize this topic, a later renaming is always possible.

[avekens]

I would also vote for "eqabcb", following @icecream17's argumentation.

[wlammen]

eqabcb seems to be the name wanted by most, so I will change the PR accordingly.