Description: Alternate proof of bicomd 226 which is shorter after expanding all parent
theorems (as of 8-Aug-2024, bicom 225 depends on bicom1 224 and sylib 221
depends on syl 17). Additionally, the labels bicom1 224 and syl 17 happen
to contain fewer characters than bicom 225
and sylib 221. However, neither
of these conditions count as a shortening according to conventions 28349.
In the first case, the criteria could easily be broken by upstream
changes, and in many cases the upstream dependency tree is nontrivial
(see orass 921 and pm2.31 922). For the latter case, theorem labels are up
to revision, so they are not counted in the size of a proof.
(Contributed by SN, 21-May-2022.) (New usage is discouraged.)
(Proof modification is discouraged.) |