shorten exexw

set.mm

@@ -17174,9 +17174,8 @@ variables and no wff metavariables (see ~ ax12wdemo for an example of
        ~ bj-exexbiex , requiring fewer axioms.  (Contributed by Gino Giotto,
        4-Nov-2024.) $)
     exexw $p |- ( E. x ph <-> E. x E. x ph ) $=
-      ( wex cbvexvw wb weq bicomd equcoms 19.8aw eximi a1i sylib biimpi exlimiv
-      impbii bitri ) ACFZBDFZTCFZABCDEGZUAUBUAUADFUBBUADBADCBAHCDCDIABEJKZLMUAT
-      DCUATHDCIBADCUDGNGOTUACTUAUCPQRS $.
+      ( wal wex weq notbid hba1w spw alimi impbii notbii df-ex 2exnaln 3bitr4i
+      wn ) ARZCFZRTCFZRACGZUBCGTUATUASBRZCDCDHABEIZJTSCSUCCDUDKLMNACOACCPQ $.
     $( $j usage 'exexw' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
   $}