reduce axioms in r19.37v (#3259)

* shorten r19.30

* revise r19.37v

---------

Co-authored-by: Wolf Lammen <[email protected]>

Author: wlammen

discouraged

@@ -17293,6 +17293,8 @@ New usage of "r19.27vOLD" is discouraged (0 uses).
 New usage of "r19.28vOLD" is discouraged (0 uses).
 New usage of "r19.29aOLD" is discouraged (0 uses).
 New usage of "r19.29anOLD" is discouraged (0 uses).
+New usage of "r19.30OLD" is discouraged (0 uses).
+New usage of "r19.37vOLD" is discouraged (0 uses).
 New usage of "r1omALT" is discouraged (0 uses).
 New usage of "r1pwALT" is discouraged (0 uses).
 New usage of "ralbiOLD" is discouraged (0 uses).
@@ -19534,6 +19536,8 @@ Proof modification of "r19.27vOLD" is discouraged (39 steps).
 Proof modification of "r19.28vOLD" is discouraged (38 steps).
 Proof modification of "r19.29aOLD" is discouraged (11 steps).
 Proof modification of "r19.29anOLD" is discouraged (35 steps).
+Proof modification of "r19.30OLD" is discouraged (75 steps).
+Proof modification of "r19.37vOLD" is discouraged (8 steps).
 Proof modification of "r1omALT" is discouraged (13 steps).
 Proof modification of "r1pwALT" is discouraged (151 steps).
 Proof modification of "ralbiOLD" is discouraged (19 steps).

set.mm

@@ -1607,6 +1607,8 @@ giving a shorter proof but depending on more axioms (namely, ~ ax-1 and
       ( wn wi con4 ax-mp ) ADBDEBAECABFG $.
   $}
 
+  $( $j usage 'con4i' avoids 'ax-1' 'ax-2'; $)
+
   ${
     con4d.1 $e |- ( ph -> ( -. ps -> -. ch ) ) $.
     $( Deduction associated with ~ con4 .  (Contributed by NM, 26-Mar-1995.) $)
@@ -1641,6 +1643,8 @@ giving a shorter proof but depending on more axioms (namely, ~ ax-1 and
       ( pm2.21i ax-mp ) ABCABDEF $.
   $}
 
+  $( $j usage 'pm2.24ii' avoids 'ax-2'; $)
+
   ${
     pm2.21d.1 $e |- ( ph -> -. ps ) $.
     $( A contradiction implies anything.  Deduction associated with ~ pm2.21 .
@@ -1729,6 +1733,8 @@ In classical logic (our logic) this is always true.  In intuitionistic
     notnotri $p |- ph $=
       ( wn pm2.21i mt4 ) ACZCZABFGCBDE $.
 
+    $( $j usage 'notnotri' avoids 'ax-2'; $)
+
     $( Alternate proof of ~ notnotri .  Inference associated with ~ notnotr .
 
        Remark: the proof via ~ notnotr and ~ ax-mp also has three essential
@@ -13084,6 +13090,8 @@ simplest antecedents (i.e., in the corresponding ordering of binary trees
   ( ( ps -> ch ) -> ( ( ( th -> ps ) -> ( ch -> ta ) ) -> ( ps -> ta ) ) ) ) $=
     ( wi jarr a2d com12 a1i ) BCFZDBFCEFZFZBEFZFFAMKNMBCEDBLGHIJ $.
 
+  $( $j usage 'minimp' avoids 'ax-3'; $)
+
   $( Derivation of Syll-Simp ( ~ jarr ) from ~ ax-mp and ~ minimp .
      (Contributed by BJ, 4-Apr-2021.)  (Proof modification is discouraged.)
      (New usage is discouraged.) $)
@@ -28919,9 +28927,18 @@ choice between (what we call) a "definitional form" where the shorter
   $}
 
   $( Restricted quantifier version of ~ 19.30 .  (Contributed by Scott Fenton,
-     25-Feb-2011.) $)
+     25-Feb-2011.)  (Proof shortened by Wolf Lammen, 18-Jun-2023.) $)
   r19.30 $p |- ( A. x e. A ( ph \/ ps ) ->
                  ( A. x e. A ph \/ E. x e. A ps ) ) $=
+    ( wo wral wn wi wrex pm2.53 orcoms ralimi ralnex biimpri imim1i orrd orcomd
+    ralim 3syl ) ABEZCDFBGZAHZCDFUACDFZACDFZHZUDBCDIZETUBCDBAUBBAJKLUAACDRUEUFU
+    DUEUFUDUFGZUCUDUCUGBCDMNOPQS $.
+
+  $( Obsolete version of ~ r19.30 as of 18-Jun-2023.  (Contributed by Scott
+     Fenton, 25-Feb-2011.)  (Proof modification is discouraged.)
+     (New usage is discouraged.) $)
+  r19.30OLD $p |- ( A. x e. A ( ph \/ ps ) ->
+                 ( A. x e. A ph \/ E. x e. A ps ) ) $=
     ( wn wi wral wrex ralim orcom df-or bitri ralbii dfrex2 orbi2i imor 3bitr4i
     wo 3imtr4i ) BEZAFZCDGTCDGZACDGZFZABRZCDGUCBCDHZRZTACDIUEUACDUEBARUAABJBAKL
     MUCUBEZRUHUCRUGUDUCUHJUFUHUCBCDNOUBUCPQS $.
@@ -28939,9 +28956,9 @@ choice between (what we call) a "definitional form" where the shorter
      20-Sep-2003.) $)
   r19.35 $p |- ( E. x e. A ( ph -> ps ) <->
                ( A. x e. A ph -> E. x e. A ps ) ) $=
-    ( wral wn wi wrex r19.26 annim ralbii df-an 3bitr3i con2bii dfrex2 3bitr4ri
-    wa imbi2i ) ACDEZBFZCDEZFZGZABGZFZCDEZFSBCDHZGUDCDHUFUCATQZCDESUAQUFUCFATCD
-    IUHUECDABJKSUALMNUGUBSBCDORUDCDOP $.
+    ( wi wrex wral pm2.27 ralimi rexim syl com12 wn rexnal pm2.21 reximi sylbir
+    ax-1 ja impbii ) ABEZCDFZACDGZBCDFZEUCUBUDUCUABEZCDGUBUDEAUECDABHIUABCDJKLU
+    CUDUBUCMAMZCDFUBACDNUFUACDABOPQBUACDBARPST $.
 
   ${
     $d x ps $.
@@ -28967,8 +28984,16 @@ choice between (what we call) a "definitional form" where the shorter
     $d x ph $.
     $( Restricted quantifier version of one direction of ~ 19.37v .  (The other
        direction holds iff ` A ` is nonempty, see ~ r19.37zv .)  (Contributed
-       by NM, 2-Apr-2004.) $)
+       by NM, 2-Apr-2004.)  Reduce axiom usage.  (Revised by Wolf Lammen,
+       18-Jun-2023.) $)
     r19.37v $p |- ( E. x e. A ( ph -> ps ) -> ( ph -> E. x e. A ps ) ) $=
+      ( wral wi wrex id ralrimivw r19.35 biimpi syl5 ) AACDEZABFCDGZBCDGZAACDAH
+      INMOFABCDJKL $.
+
+    $( Obsolete version of ~ r19.37v as of 18-Jun-2023.  (Contributed by NM,
+       2-Apr-2004.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    r19.37vOLD $p |- ( E. x e. A ( ph -> ps ) -> ( ph -> E. x e. A ps ) ) $=
       ( nfv r19.37 ) ABCDACEF $.
   $}