Minimize propositional calculus theorems (#5081)

Author: EricSchmidt-119

set.mm

@@ -11224,9 +11224,8 @@ This definition (in the form of ~ dfifp2 ) appears in Section II.24 of
   $( Rearrangement of 6 conjuncts.  (Contributed by NM, 13-Mar-1995.) $)
   an6 $p |- ( ( ( ph /\ ps /\ ch ) /\ ( th /\ ta /\ et ) ) <->
               ( ( ph /\ th ) /\ ( ps /\ ta ) /\ ( ch /\ et ) ) ) $=
-    ( wa w3a an4 anbi1i bitri df-3an anbi12i 3bitr4i ) ABGZCGZDEGZFGZGZADGZBEGZ
-    GZCFGZGZABCHZDEFHZGTUAUCHSOQGZUCGUDOCQFIUGUBUCABDEIJKUEPUFRABCLDEFLMTUAUCLN
-    $.
+    ( wa w3a an4 bianbi df-3an anbi12i 3bitr4i ) ABGZCGZDEGZFGZGZADGZBEGZGZCFGZ
+    GABCHZDEFHZGSTUBHRNPGUBUANCPFIABDEIJUCOUDQABCKDEFKLSTUBKM $.
 
   $( Analogue of ~ an4 for triple conjunction.  (Contributed by Scott Fenton,
      16-Mar-2011.)  (Proof shortened by Andrew Salmon, 25-May-2011.) $)
@@ -11484,8 +11483,8 @@ This definition (in the form of ~ dfifp2 ) appears in Section II.24 of
     $( Deduction for elimination by cases.  (Contributed by NM,
        22-Apr-1994.) $)
     ecase23d $p |- ( ph -> ps ) $=
-      ( wo wn ioran sylanbrc w3o 3orass sylib ord mt3d ) ABCDHZACIDIQIEFCDJKABQ
-      ABCDLBQHGBCDMNOP $.
+      ( wo w3o 3orass sylib wn ioran sylanbrc olcnd ) ABCDHZABCDIBPHGBCDJKACLDL
+      PLEFCDMNO $.
   $}
 
   ${
@@ -11922,7 +11921,7 @@ Principia Mathematica (1927), Russell and Whitehead used the Sheffer
   $( This lemma specializes ~ biimt suitably for the proof of ~ norass .
      (Contributed by Wolf Lammen, 18-Dec-2023.) $)
   norasslem2 $p |- ( ph -> ( ps <-> ( ( ph \/ ch ) -> ps ) ) ) $=
-    ( wo wi wb orc biimt syl ) AACDZBJBEFACGJBHI $.
+    ( wo wi wb biimt orcs ) ACBACDZBEFIBGH $.
 
   $( This lemma specializes ~ biorf suitably for the proof of ~ norass .
      (Contributed by Wolf Lammen, 18-Dec-2023.) $)