Remaining proposed syl renames (groups 3 and 4)

[jkingdon]

These had their roots in a proposal by Norm which has received some refinement, discussion, and action since.

The proposed changes are listed in changes-set.txt and the division into groups is from #4332 (comment) . Group 1 from that comment is done, #4504 is about group 2, and this issue is for groups 3 and 4.

The proposed renames in groups 3 and 4 are:

proposed  syldc     imtrdcom
proposed  syldd     imtrdd
proposed  sylbb     bitriim
proposed  sylbbr    bitrriim
proposed  sylbb1    bitr3iim
proposed  sylbb2    bitr4iim
proposed  syl5com   imtridcom
proposed  syl56     imtridi
proposed  syl5d     imtridd
proposed  syl5ibcom imbitridcom
proposed  syl5ibrcom imbitrridcom
proposed  syl6com   imtrdicom
proposed  syl6d     imtrdid
proposed  syl       imtri       (analogous to *bitr*, sstri, etc.)
                                there is less agreement on renaming syl
                                than others here
proposed  syl5      imtrid      alternate proposal: sylid
proposed  syl6      imtrdi      alternate proposal: syldi

Some of these seem relatively clear in terms of what name matches our conventions; some of them are on this list because they are a bit more ad hoc but seem better than the existing names. In particular, getting rid of the numbers 5 and 6 in the context of syl naming might be a desirable goal, which would call for doing these renames and the ones from #4504 as well as syl6an , syl6mpi , syl6c , syl6ci and (in Alan Sare's mathbox) syl5imp and syl5impVD.

The theorem syl is a bit of a special case because it is referenced in the metamath book and thus might benefit from a comment analogous to the one at https://us.metamath.org/mpeuni/trud.html .

Feel free to make suggestions for alternate names or any of these that aren't a good idea. I would recommend that we do the renames in #4504 before any of these.

However, to the extent there was a consensus in the discussion in #4332 it seemed to be that we wanted to rename these somehow, so I guess I'm operating under the assumption that for most/all of them we do want a new name, even if I'm more uncertain about whether there are better choices for some of the new names.

[benjub]

I'm in favor of all these renamings, thank you for the clear exposition.

Among these, I think it is especially important to rename syl: this has the same consistency and mnemonics advantages as the other labels in this list, and moreover, it removes this "misnomer" since "syl" is generally used in propositional calculus to denote the closed form and not the inference as in the current version of set.mm. See #4332 (comment)