moved theorems in earlier $a-interval

GinoGiotto · Aug 23, 2023 · a17dbc1 · a17dbc1
1 parent e6b4f48
commit a17dbc1
Showing 1 changed file with 89 additions and 89 deletions.
diff --git a/set.mm b/set.mm
@@ -18029,6 +18029,12 @@ Converse of the inference rule of (universal) generalization ~ ax-gen .
       ( wal sp syl ) ACEABACFDG $.
   $}
 
+  $( Formula-building lemma for use with the Distinctor Reduction Theorem.
+     Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint).  (Contributed
+     by NM, 27-Feb-2005.) $)
+  drsb2 $p |- ( A. x x = y -> ( [ x / z ] ph <-> [ y / z ] ph ) ) $=
+    ( weq wsb wb sbequ sps ) BCEADBFADCFGBABCDHI $.
+
   $( A double specialization (see ~ sp ).  Another double specialization,
      closer to PM*11.1, is ~ 2stdpc4 .  (Contributed by BJ, 15-Sep-2018.) $)
   2sp $p |- ( A. x A. y ph -> ph ) $=
@@ -18739,6 +18745,27 @@ Converse of the inference rule of (universal) generalization ~ ax-gen .
       ( wnf wsb wb sbft ax-mp ) ABEABCFAGDABCHI $.
   $}
 
+  $( Substitution has no effect on a bound variable.  (Contributed by NM,
+     1-Jul-2005.) $)
+  sbf2 $p |- ( [ y / x ] A. x ph <-> A. x ph ) $=
+    ( wal nfa1 sbf ) ABDBCABEF $.
+
+  ${
+    sbh.1 $e |- ( ph -> A. x ph ) $.
+    $( Substitution for a variable not free in a wff does not affect it.
+       (Contributed by NM, 14-May-1993.) $)
+    sbh $p |- ( [ y / x ] ph <-> ph ) $=
+      ( nf5i sbf ) ABCABDEF $.
+  $}
+
+  ${
+    nfs1f.1 $e |- F/ x ph $.
+    $( If ` x ` is not free in ` ph ` , it is not free in ` [ y / x ] ph ` .
+       (Contributed by Mario Carneiro, 11-Aug-2016.) $)
+    nfs1f $p |- F/ x [ y / x ] ph $=
+      ( wsb sbf nfxfr ) ABCEABABCDFDG $.
+  $}
+
   ${
     $d x y $.
     $( Two equivalent ways of expressing the proper substitution of ` y ` for
@@ -19023,6 +19050,68 @@ Converse of the inference rule of (universal) generalization ~ ax-gen .
     ( wsb wi wn sbn pm2.21 sbimi sylbir ax-1 ja ) ACDEZBCDEABFZCDEZNGAGZCDEPACD
     HQOCDABIJKBOCDBALJM $.
 
+  $( Implication inside and outside of a substitution are equivalent.
+     (Contributed by NM, 14-May-1993.) $)
+  sbim $p |- ( [ y / x ] ( ph -> ps ) <-> ( [ y / x ] ph -> [ y / x ] ps ) ) $=
+    ( wi wsb sbi1 sbi2 impbii ) ABECDFACDFBCDFEABCDGABCDHI $.
+
+  ${
+    sbrim.1 $e |- F/ x ph $.
+    $( Substitution in an implication with a variable not free in the
+       antecedent affects only the consequent.  (Contributed by NM,
+       2-Jun-1993.)  (Revised by Mario Carneiro, 4-Oct-2016.) $)
+    sbrim $p |- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) ) $=
+      ( wi wsb sbim sbf imbi1i bitri ) ABFCDGACDGZBCDGZFAMFABCDHLAMACDEIJK $.
+  $}
+
+  ${
+    sblim.1 $e |- F/ x ps $.
+    $( Substitution in an implication with a variable not free in the
+       consequent affects only the antecedent.  (Contributed by NM,
+       14-Nov-2013.)  (Revised by Mario Carneiro, 4-Oct-2016.) $)
+    sblim $p |- ( [ y / x ] ( ph -> ps ) <-> ( [ y / x ] ph -> ps ) ) $=
+      ( wi wsb sbim sbf imbi2i bitri ) ABFCDGACDGZBCDGZFLBFABCDHMBLBCDEIJK $.
+  $}
+
+  $( Disjunction inside and outside of a substitution are equivalent.
+     (Contributed by NM, 29-Sep-2002.) $)
+  sbor $p |- ( [ y / x ] ( ph \/ ps ) <-> ( [ y / x ] ph \/ [ y / x ] ps ) ) $=
+    ( wn wi wsb wo sbim sbn imbi1i bitri df-or sbbii 3bitr4i ) AEZBFZCDGZACDGZE
+    ZBCDGZFZABHZCDGSUAHRPCDGZUAFUBPBCDIUDTUAACDJKLUCQCDABMNSUAMO $.
+
+  $( Equivalence inside and outside of a substitution are equivalent.
+     (Contributed by NM, 14-May-1993.) $)
+  sbbi $p |- ( [ y / x ] ( ph <-> ps )
+     <-> ( [ y / x ] ph <-> [ y / x ] ps ) ) $=
+    ( wb wsb wi wa dfbi2 sbbii sbim anbi12i sban 3bitr4i bitri ) ABEZCDFABGZBAG
+    ZHZCDFZACDFZBCDFZEZPSCDABIJQCDFZRCDFZHUAUBGZUBUAGZHTUCUDUFUEUGABCDKBACDKLQR
+    CDMUAUBINO $.
+
+  ${
+    sblbis.1 $e |- ( [ y / x ] ph <-> ps ) $.
+    $( Introduce left biconditional inside of a substitution.  (Contributed by
+       NM, 19-Aug-1993.) $)
+    sblbis $p |- ( [ y / x ] ( ch <-> ph ) <-> ( [ y / x ] ch <-> ps ) ) $=
+      ( wb wsb sbbi bibi2i bitri ) CAGDEHCDEHZADEHZGLBGCADEIMBLFJK $.
+  $}
+
+  ${
+    sbrbis.1 $e |- ( [ y / x ] ph <-> ps ) $.
+    $( Introduce right biconditional inside of a substitution.  (Contributed by
+       NM, 18-Aug-1993.) $)
+    sbrbis $p |- ( [ y / x ] ( ph <-> ch ) <-> ( ps <-> [ y / x ] ch ) ) $=
+      ( wb wsb sbbi bibi1i bitri ) ACGDEHADEHZCDEHZGBMGACDEILBMFJK $.
+  $}
+
+  ${
+    sbrbif.1 $e |- F/ x ch $.
+    sbrbif.2 $e |- ( [ y / x ] ph <-> ps ) $.
+    $( Introduce right biconditional inside of a substitution.  (Contributed by
+       NM, 18-Aug-1993.)  (Revised by Mario Carneiro, 4-Oct-2016.) $)
+    sbrbif $p |- ( [ y / x ] ( ph <-> ch ) <-> ( ps <-> ch ) ) $=
+      ( wb wsb sbrbis sbf bibi2i bitri ) ACHDEIBCDEIZHBCHABCDEGJNCBCDEFKLM $.
+  $}
+
   ${
     $d x y $.
     $( Obsolete version of ~ sbn as of 8-Jul-2023.  Substitution is not
@@ -20566,33 +20655,6 @@ requires either a disjoint variable condition ( ~ sb56 ) or a non-freeness
   sbequOLD $p |- ( x = y -> ( [ x / z ] ph <-> [ y / z ] ph ) ) $=
     ( weq wsb sbequi wi equcoms impbid ) BCEADBFZADCFZABCDGLKHCBACBDGIJ $.
 
-  $( Formula-building lemma for use with the Distinctor Reduction Theorem.
-     Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint).  (Contributed
-     by NM, 27-Feb-2005.) $)
-  drsb2 $p |- ( A. x x = y -> ( [ x / z ] ph <-> [ y / z ] ph ) ) $=
-    ( weq wsb wb sbequ sps ) BCEADBFADCFGBABCDHI $.
-
-  ${
-    sbh.1 $e |- ( ph -> A. x ph ) $.
-    $( Substitution for a variable not free in a wff does not affect it.
-       (Contributed by NM, 14-May-1993.) $)
-    sbh $p |- ( [ y / x ] ph <-> ph ) $=
-      ( nf5i sbf ) ABCABDEF $.
-  $}
-
-  $( Substitution has no effect on a bound variable.  (Contributed by NM,
-     1-Jul-2005.) $)
-  sbf2 $p |- ( [ y / x ] A. x ph <-> A. x ph ) $=
-    ( wal nfa1 sbf ) ABDBCABEF $.
-
-  ${
-    nfs1f.1 $e |- F/ x ph $.
-    $( If ` x ` is not free in ` ph ` , it is not free in ` [ y / x ] ph ` .
-       (Contributed by Mario Carneiro, 11-Aug-2016.) $)
-    nfs1f $p |- F/ x [ y / x ] ph $=
-      ( wsb sbf nfxfr ) ABCEABABCDFDG $.
-  $}
-
   ${
     sb6x.1 $e |- F/ x ph $.
     $( Equivalence involving substitution for a variable not free.
@@ -21159,35 +21221,6 @@ proposition with a distinct variable (closed form of ~ nfsb4 ).
   spsbimOLD $p |- ( A. x ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) ) $=
     ( wi wal wsb stdpc4 sbi1 syl ) ABEZCFKCDGACDGBCDGEKCDHABCDIJ $.
 
-  $( Implication inside and outside of a substitution are equivalent.
-     (Contributed by NM, 14-May-1993.) $)
-  sbim $p |- ( [ y / x ] ( ph -> ps ) <-> ( [ y / x ] ph -> [ y / x ] ps ) ) $=
-    ( wi wsb sbi1 sbi2 impbii ) ABECDFACDFBCDFEABCDGABCDHI $.
-
-  ${
-    sbrim.1 $e |- F/ x ph $.
-    $( Substitution in an implication with a variable not free in the
-       antecedent affects only the consequent.  (Contributed by NM,
-       2-Jun-1993.)  (Revised by Mario Carneiro, 4-Oct-2016.) $)
-    sbrim $p |- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) ) $=
-      ( wi wsb sbim sbf imbi1i bitri ) ABFCDGACDGZBCDGZFAMFABCDHLAMACDEIJK $.
-  $}
-
-  ${
-    sblim.1 $e |- F/ x ps $.
-    $( Substitution in an implication with a variable not free in the
-       consequent affects only the antecedent.  (Contributed by NM,
-       14-Nov-2013.)  (Revised by Mario Carneiro, 4-Oct-2016.) $)
-    sblim $p |- ( [ y / x ] ( ph -> ps ) <-> ( [ y / x ] ph -> ps ) ) $=
-      ( wi wsb sbim sbf imbi2i bitri ) ABFCDGACDGZBCDGZFLBFABCDHMBLBCDEIJK $.
-  $}
-
-  $( Disjunction inside and outside of a substitution are equivalent.
-     (Contributed by NM, 29-Sep-2002.) $)
-  sbor $p |- ( [ y / x ] ( ph \/ ps ) <-> ( [ y / x ] ph \/ [ y / x ] ps ) ) $=
-    ( wn wi wsb wo sbim sbn imbi1i bitri df-or sbbii 3bitr4i ) AEZBFZCDGZACDGZE
-    ZBCDGZFZABHZCDGSUAHRPCDGZUAFUBPBCDIUDTUAACDJKLUCQCDABMNSUAMO $.
-
   $( Obsolete version of ~ sban as of 13-Aug-2023.  Conjunction inside and
      outside of a substitution are equivalent.  (Contributed by NM,
      14-May-1993.)  (New usage is discouraged.)
@@ -21198,46 +21231,13 @@ proposition with a distinct variable (closed form of ~ nfsb4 ).
     CDGZACDGZBCDGZEZFZEABHZCDGUAUBHTRCDGZUDRCDIUFUAQCDGZFUDAQCDJUGUCUABCDIKLMUE
     SCDABNOUAUBNP $.
 
-  $( Equivalence inside and outside of a substitution are equivalent.
-     (Contributed by NM, 14-May-1993.) $)
-  sbbi $p |- ( [ y / x ] ( ph <-> ps )
-     <-> ( [ y / x ] ph <-> [ y / x ] ps ) ) $=
-    ( wb wsb wi wa dfbi2 sbbii sbim anbi12i sban 3bitr4i bitri ) ABEZCDFABGZBAG
-    ZHZCDFZACDFZBCDFZEZPSCDABIJQCDFZRCDFZHUAUBGZUBUAGZHTUCUDUFUEUGABCDKBACDKLQR
-    CDMUAUBINO $.
-
   $( Obsolete version of ~ spsbbi as of 6-Jul-2023.  Specialization of
      biconditional.  (Contributed by NM, 2-Jun-1993.)
      (Proof modification is discouraged.)  (New usage is discouraged.) $)
   spsbbiOLD $p |- ( A. x ( ph <-> ps )
                               -> ( [ y / x ] ph <-> [ y / x ] ps ) ) $=
     ( wb wal wsb stdpc4 sbbi sylib ) ABEZCFKCDGACDGBCDGEKCDHABCDIJ $.
 
-  ${
-    sblbis.1 $e |- ( [ y / x ] ph <-> ps ) $.
-    $( Introduce left biconditional inside of a substitution.  (Contributed by
-       NM, 19-Aug-1993.) $)
-    sblbis $p |- ( [ y / x ] ( ch <-> ph ) <-> ( [ y / x ] ch <-> ps ) ) $=
-      ( wb wsb sbbi bibi2i bitri ) CAGDEHCDEHZADEHZGLBGCADEIMBLFJK $.
-  $}
-
-  ${
-    sbrbis.1 $e |- ( [ y / x ] ph <-> ps ) $.
-    $( Introduce right biconditional inside of a substitution.  (Contributed by
-       NM, 18-Aug-1993.) $)
-    sbrbis $p |- ( [ y / x ] ( ph <-> ch ) <-> ( ps <-> [ y / x ] ch ) ) $=
-      ( wb wsb sbbi bibi1i bitri ) ACGDEHADEHZCDEHZGBMGACDEILBMFJK $.
-  $}
-
-  ${
-    sbrbif.1 $e |- F/ x ch $.
-    sbrbif.2 $e |- ( [ y / x ] ph <-> ps ) $.
-    $( Introduce right biconditional inside of a substitution.  (Contributed by
-       NM, 18-Aug-1993.)  (Revised by Mario Carneiro, 4-Oct-2016.) $)
-    sbrbif $p |- ( [ y / x ] ( ph <-> ch ) <-> ( ps <-> ch ) ) $=
-      ( wb wsb sbrbis sbf bibi2i bitri ) ACHDEIBCDEIZHBCHABCDEGJNCBCDEFKLM $.
-  $}
-
   $( Elimination of equality from antecedent after substitution.  (Contributed
      by NM, 5-Aug-1993.)  Reduce dependencies on axioms.  (Revised by Wolf
      Lammen, 28-Jul-2018.)  Revise ~ df-sb .  (Revised by Wolf Lammen,