naming of syl theorems

[Jim Kingdon]

Most theorems which involve applying transitivity are named according to
a pattern

XXYYtr

where XX and YY are abbreviations for what kind of theorem this is and
then the usual suffixes apply. Examples:

eqeltrd

sseqtri

And if XX and YY are the same the abbreviation is only listed once, for
example:

sstri

bitrd

.... and many others.

One notable family of theorems that do not use this convention are the
various theorems named with syl (syl, syl5, syl6, sylbi, etc). Many
years ago, Norm proposed that we should use the "tr" convention for
these too. To quote directly (in text now in changes-set.txt):

  This is part of an ongoing project to improve naming consistency. . . .

  PROPOSED:
  Date      Old       New         Notes
  proposed  syl       imtri       (analogous to *bitr*, sstri, etc.)
  proposed  sylib     imbitri     etc.
  proposed  sylbid    biimtrd     etc.
  proposed  sylbird   biimtrrd    etc.
  proposed  syl5*     *trid       (syl5bi -> biimtrid; syl5eqel ->
eqeltrid;etc.)
  proposed  syl6*     *trdi

This is obviously a big change in the sense that the theorems to be
renamed are some of the most commonly used theorems in set.mm. But the
more I have been thinking about this the more I like the idea and am
pretty sure that once I got used to it the new names would be quite
natural and fit nicely with the many theorems which already use the "tr"
convention.

There's an issue here: https://github.com/metamath/set.mm/pull/3556
which proposes new names for individual theorems, starting with the
current *syl5* theorems. But it hasn't gotten enough discussion
(positive, negative, or otherwise) to either go ahead, formulate an
alternative proposal, decide we like the status quo, or whatever. Even
go ahead I suppose has multiple sub-options: to go ahead fairly quickly
(as we did with the mpt2 -> mpo renames) or go ahead more slowly (maybe
state a plan to do it over time, or whatever form that would take).