shorten sbhypf (#4600)

discouraged

@@ -19026,6 +19026,7 @@ New usage of "sbequ5" is discouraged (0 uses).
 New usage of "sbequ6" is discouraged (0 uses).
 New usage of "sbequ8" is discouraged (0 uses).
 New usage of "sbhb" is discouraged (0 uses).
+New usage of "sbhypfOLD" is discouraged (0 uses).
 New usage of "sbid2" is discouraged (2 uses).
 New usage of "sbid2v" is discouraged (0 uses).
 New usage of "sbidm" is discouraged (0 uses).
@@ -21328,6 +21329,7 @@ Proof modification of "sbcoreleleqVD" is discouraged (176 steps).
 Proof modification of "sbcrexgOLD" is discouraged (77 steps).
 Proof modification of "sbcssgVD" is discouraged (229 steps).
 Proof modification of "sbequ2OLD" is discouraged (75 steps).
+Proof modification of "sbhypfOLD" is discouraged (58 steps).
 Proof modification of "sbn1ALT" is discouraged (41 steps).
 Proof modification of "sbrimOLD" is discouraged (33 steps).
 Proof modification of "sbsbc" is discouraged (21 steps).

set.mm

@@ -32638,10 +32638,10 @@ general is seen either by substitution (when the variable ` V ` has no
     ceqsex3v $p |- ( E. x E. y E. z ( ( x = A /\ y = B /\ z = C ) /\ ph )
                  <-> th ) $=
       ( cv wceq wa wex anass 3anass anbi1i df-3an anbi2i 3bitr4i 2exbii 19.42vv
-      w3a bitri exbii 3anbi3d 2exbidv ceqsexv ceqsex2v ) EQHRZFQIRZGQJRZUIZASZG
-      TFTZETUPUQURAUIZGTFTZSZETZDVAVDEVAUPVBSZGTFTVDUTVFFGUPUQURSZSZASUPVGASZSU
-      TVFUPVGAUAUSVHAUPUQURUBUCVBVIUPUQURAUDUEUFUGUPVBFGUHUJUKVEUQURBUIZGTFTZDV
-      CVKEHKUPVBVJFGUPABUQURNULUMUNBCDFGIJLMOPUOUJUJ $.
+      w3a bitri exbii 3anbi3d 2exbidv ceqsexv ceqsex2v 3bitri ) EQHRZFQIRZGQJRZ
+      UIZASZGTFTZETUQURUSAUIZGTFTZSZETURUSBUIZGTFTZDVBVEEVBUQVCSZGTFTVEVAVHFGUQ
+      URUSSZSZASUQVIASZSVAVHUQVIAUAUTVJAUQURUSUBUCVCVKUQURUSAUDUEUFUGUQVCFGUHUJ
+      UKVDVGEHKUQVCVFFGUQABURUSNULUMUNBCDFGIJLMOPUOUP $.
   $}
 
   ${
@@ -32689,11 +32689,11 @@ general is seen either by substitution (when the variable ` V ` has no
           ( ( x = A /\ y = B /\ z = C ) /\ ( w = D /\ v = E /\ u = F ) /\ ph )
                  <-> ze ) $=
       ( cv wceq w3a wex wa 3anass 3exbii 19.42vvv bitri anbi2d 3exbidv ceqsex3v
-      ) HULNUMZIULOUMZJULPUMZUNZKULQUMLULRUMMULSUMUNZAUNZMUOLUOKUOZJUOIUOHUOVGV
-      HAUPZMUOLUOKUOZUPZJUOIUOHUOZGVJVMHIJVJVGVKUPZMUOLUOKUOVMVIVOKLMVGVHAUQURV
-      GVKKLMUSUTURVNVHDUPZMUOLUOKUOZGVLVHBUPZMUOLUOKUOVHCUPZMUOLUOKUOVQHIJNOPTU
-      AUBVDVKVRKLMVDABVHUFVAVBVEVRVSKLMVEBCVHUGVAVBVFVSVPKLMVFCDVHUHVAVBVCDEFGK
-      LMQRSUCUDUEUIUJUKVCUTUT $.
+      3bitri ) HULNUMZIULOUMZJULPUMZUNZKULQUMLULRUMMULSUMUNZAUNZMUOLUOKUOZJUOIU
+      OHUOVHVIAUPZMUOLUOKUOZUPZJUOIUOHUOVIDUPZMUOLUOKUOZGVKVNHIJVKVHVLUPZMUOLUO
+      KUOVNVJVQKLMVHVIAUQURVHVLKLMUSUTURVMVIBUPZMUOLUOKUOVICUPZMUOLUOKUOVPHIJNO
+      PTUAUBVEVLVRKLMVEABVIUFVAVBVFVRVSKLMVFBCVIUGVAVBVGVSVOKLMVGCDVIUHVAVBVCDE
+      FGKLMQRSUCUDUEUIUJUKVCVD $.
   $}
 
   ${
@@ -32723,15 +32723,15 @@ general is seen either by substitution (when the variable ` V ` has no
               ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) )
          /\ ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) ) /\ ph ) <-> rh ) $=
       ( cv wceq wa w3a 19.42vv 2exbii bitri 3anass df-3an anbi2i bitr4i 3bitr4i
-      wex 3anbi3d 4exbidv ceqsex4v ) JVBQVCZKVBRVCZVDZLVBSVCZMVBTVCZVDZVDZNVBUA
-      VCOVBUBVCVDZPVBUCVCUEVBUDVCVDZVDZAVEZUEVNPVNZOVNNVNZMVNLVNZKVNJVNVTWCWEWF
-      AVEZUEVNPVNZOVNNVNZVEZMVNLVNZKVNJVNZIWKWPJKWJWOLMWDWLVDZUEVNPVNZOVNNVNZWD
-      WNVDZWJWOWTWDWMVDZOVNNVNXAWSXBNOWDWLPUEVFVGWDWMNOVFVHWIWSNOWHWRPUEWHWDWGA
-      VDZVDWRWDWGAVIWLXCWDWEWFAVJVKVLVGVGVTWCWNVJVMVGVGWQWEWFEVEZUEVNPVNOVNNVNZ
-      IWNWEWFBVEZUEVNPVNOVNNVNWEWFCVEZUEVNPVNOVNNVNWEWFDVEZUEVNPVNOVNNVNXEJKLMQ
-      RSTUFUGUHUIVRWLXFNOPUEVRABWEWFUNVOVPVSXFXGNOPUEVSBCWEWFUOVOVPWAXGXHNOPUEW
-      ACDWEWFUPVOVPWBXHXDNOPUEWBDEWEWFUQVOVPVQEFGHINOPUEUAUBUCUDUJUKULUMURUSUTV
-      AVQVHVH $.
+      wex 3anbi3d 4exbidv ceqsex4v 3bitri ) JVBQVCZKVBRVCZVDZLVBSVCZMVBTVCZVDZV
+      DZNVBUAVCOVBUBVCVDZPVBUCVCUEVBUDVCVDZVDZAVEZUEVNPVNZOVNNVNZMVNLVNZKVNJVNW
+      AWDWFWGAVEZUEVNPVNZOVNNVNZVEZMVNLVNZKVNJVNWFWGEVEZUEVNPVNOVNNVNZIWLWQJKWK
+      WPLMWEWMVDZUEVNPVNZOVNNVNZWEWOVDZWKWPXBWEWNVDZOVNNVNXCXAXDNOWEWMPUEVFVGWE
+      WNNOVFVHWJXANOWIWTPUEWIWEWHAVDZVDWTWEWHAVIWMXEWEWFWGAVJVKVLVGVGWAWDWOVJVM
+      VGVGWOWFWGBVEZUEVNPVNOVNNVNWFWGCVEZUEVNPVNOVNNVNWFWGDVEZUEVNPVNOVNNVNWSJK
+      LMQRSTUFUGUHUIVSWMXFNOPUEVSABWFWGUNVOVPVTXFXGNOPUEVTBCWFWGUOVOVPWBXGXHNOP
+      UEWBCDWFWGUPVOVPWCXHWRNOPUEWCDEWFWGUQVOVPVQEFGHINOPUEUAUBUCUDUJUKULUMURUS
+      UTVAVQVR $.
   $}
 
   ${
@@ -32782,8 +32782,15 @@ general is seen either by substitution (when the variable ` V ` has no
     sbhypf.2 $e |- ( x = A -> ( ph <-> ps ) ) $.
     $( Introduce an explicit substitution into an implicit substitution
        hypothesis.  See also ~ csbhypf .  (Contributed by Raph Levien,
-       10-Apr-2004.) $)
+       10-Apr-2004.)  (Proof shortened by Wolf Lammen, 25-Jan-2025.) $)
     sbhypf $p |- ( y = A -> ( [ y / x ] ph <-> ps ) ) $=
+      ( cv wceq wsb wb sbimi eqsb1 sbf sblbis 3imtr3i ) CHEIZCDJABKZCDJDHEIACDJ
+      BKQRCDGLCDEMBBACDBCDFNOP $.
+
+    $( Obsolete version of ~ sbhypf as of 25-Jan-2025.  (Contributed by Raph
+       Levien, 10-Apr-2004.)  (New usage is discouraged.)
+       (Proof modification is discouraged.) $)
+    sbhypfOLD $p |- ( y = A -> ( [ y / x ] ph <-> ps ) ) $=
       ( cv wceq wa wex wsb wb eqeq1 equsexvw nfs1v nfbi sbequ12 bicomd sylan9bb
       exlimi sylbir ) DHZEIZCHZUCIZUEEIZJZCKACDLZBMZUGUDCDUEUCENOUHUJCUIBCACDPF
       QUFUIAUGBUFAUIACDRSGTUAUB $.