shorten proofs

set.mm

@@ -20062,9 +20062,8 @@ Corresponds to the dual of Axiom (B) of modal logic.  (Contributed by NM,
     $( Distribute universal quantifiers.  (Contributed by NM, 12-Aug-1993.)
        Avoid ~ ax-10 .  (Revised by Gino Giotto, 21-Nov-2024.) $)
     aaan $p |- ( A. x A. y ( ph /\ ps ) <-> ( A. x ph /\ A. y ps ) ) $=
-      ( wa wal 19.26-2 sp alimi anim12i sylbi nf5ri hbal biimpri alanimi sylan2
-      19.28 impbii ) ABGDHZCHZACHZBDHZGZUBADHZCHZUDCHZGUEABCDIUGUCUHUDUFACADJKU
-      DCJLMUDUCUHUBBCDBCFNOAUDUACUAAUDGABDESPQRT $.
+      ( wa wal 19.26-2 19.3 albii alcom bitri anbi12i ) ABGDHCHADHZCHZBDHZCHZGA
+      CHZQGABCDIPSRQOACADEJKRBCHZDHQBCDLTBDBCFJKMNM $.
     $( $j usage 'aaan' avoids 'ax-10'; $)
 
     $( Obsolete version of ~ aaan as of 21-Nov-2024.  (Contributed by NM,
@@ -20081,10 +20080,8 @@ Corresponds to the dual of Axiom (B) of modal logic.  (Contributed by NM,
     $( Distribute existential quantifiers.  (Contributed by NM, 8-Aug-1994.)
        Avoid ~ ax-10 .  (Revised by Gino Giotto, 21-Nov-2024.) $)
     eeor $p |- ( E. x E. y ( ph \/ ps ) <-> ( E. x ph \/ E. y ps ) ) $=
-      ( wo wex wn wal wa df-ex alnex ioran albii bitr3i notbii ianor nfn aaan
-      orbi12i 3bitr4i 3bitri ) ABGZDHZCHUEIZCJZIAIZBIZKZDJZCJZIZACHZBDHZGZUECLU
-      GULUFUKCUFUDIZDJUKUDDMUQUJDABNOPOQUHCJZUIDJZKZIURIZUSIZGUMUPURUSRULUTUHUI
-      CDADESBCFSTQUNVAUOVBACLBDLUAUBUC $.
+      ( wo wex 19.43 exbii 19.9 excom bitri orbi12i ) ABGDHZCHADHZBDHZGZCHZACHZ
+      QGZORCABDIJSPCHZQCHZGUAPQCIUBTUCQPACADEKJUCBCHZDHQBCDLUDBDBCFKJMNMM $.
     $( $j usage 'eeor' avoids 'ax-10'; $)
 
     $( Obsolete version of ~ eeor as of 21-Nov-2024.  (Contributed by NM,