shorten spcimdv (metamath#3424)

GinoGiotto · Aug 25, 2023 · 720f8b4 · 720f8b4
1 parent 1a1c3f7
commit 720f8b4
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/set.mm b/set.mm
@@ -31802,9 +31802,9 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
          by Mario Carneiro, 4-Jan-2017.)  Avoid ~ ax-10 and ~ ax-11 .  (Revised
          by Gino Giotto, 20-Aug-2023.) $)
       spcimdv $p |- ( ph -> ( A. x ps -> ch ) ) $=
-        ( cv wceq wi wal wcel ex alrimiv cvv elex wex isset exim syl5bi 19.36v
-        syl6ib syl5 sylc ) ADIEJZBCKZKZDLZEFMZBDLCKZAUHDAUFUGHNOGUJEPMZUIUKEFQU
-        IULUGDRZUKULUFDRUIUMDESUFUGDTUABCDUBUCUDUE $.
+        ( wi wex wal cv wceq ex alrimiv cvv wcel elex syl sylib isset exim sylc
+        19.36v ) ABCIZDJZBDKCIADLEMZUEIZDKUGDJZUFAUHDAUGUEHNOAEPQZUIAEFQUJGEFRS
+        DEUATUGUEDUBUCBCDUDT $.
     $}
 
     ${