shorten pm19.38 nelne1 nelne2 (#3174)

* shorten pm19.38 nelne1 nelne2

* add missing tags

* update discouraged

---------

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

Author: wlammen

discouraged

@@ -16631,6 +16631,8 @@ New usage of "nannanOLD" is discouraged (0 uses).
 New usage of "nannotOLD" is discouraged (0 uses).
 New usage of "natded" is discouraged (0 uses).
 New usage of "negexsr" is discouraged (0 uses).
+New usage of "nelne1OLD" is discouraged (0 uses).
+New usage of "nelne2OLD" is discouraged (0 uses).
 New usage of "nexmoOLD" is discouraged (0 uses).
 New usage of "nf5dvOLD" is discouraged (0 uses).
 New usage of "nf5riOLD" is discouraged (0 uses).
@@ -17241,6 +17243,7 @@ New usage of "pm10.252" is discouraged (0 uses).
 New usage of "pm11.07" is discouraged (0 uses).
 New usage of "pm110.643ALT" is discouraged (0 uses).
 New usage of "pm13.183OLD" is discouraged (0 uses).
+New usage of "pm13.18OLD" is discouraged (0 uses).
 New usage of "pm2.21ddALT" is discouraged (0 uses).
 New usage of "pm2.43bgbi" is discouraged (0 uses).
 New usage of "pm2.43cbi" is discouraged (2 uses).
@@ -19447,6 +19450,8 @@ Proof modification of "nanbi1OLD" is discouraged (32 steps).
 Proof modification of "nancomOLD" is discouraged (26 steps).
 Proof modification of "nannanOLD" is discouraged (32 steps).
 Proof modification of "nannotOLD" is discouraged (17 steps).
+Proof modification of "nelne1OLD" is discouraged (26 steps).
+Proof modification of "nelne2OLD" is discouraged (26 steps).
 Proof modification of "nexmoOLD" is discouraged (60 steps).
 Proof modification of "nf5dvOLD" is discouraged (20 steps).
 Proof modification of "nf5riOLD" is discouraged (13 steps).
@@ -19567,6 +19572,7 @@ Proof modification of "pilem3OLD" is discouraged (583 steps).
 Proof modification of "pm110.643" is discouraged (72 steps).
 Proof modification of "pm110.643ALT" is discouraged (35 steps).
 Proof modification of "pm13.183OLD" is discouraged (111 steps).
+Proof modification of "pm13.18OLD" is discouraged (28 steps).
 Proof modification of "pm2.21ddALT" is discouraged (10 steps).
 Proof modification of "pm2.43bgbi" is discouraged (16 steps).
 Proof modification of "pm2.43cbi" is discouraged (34 steps).

set.mm

@@ -27081,8 +27081,14 @@ choice between (what we call) a "definitional form" where the shorter
     MHJK $.
 
   $( Theorem *13.18 in [WhiteheadRussell] p. 178.  (Contributed by Andrew
-     Salmon, 3-Jun-2011.) $)
+     Salmon, 3-Jun-2011.)  (Proof shortened by Wolf Lammen, 14-May-2023.) $)
   pm13.18 $p |- ( ( A = B /\ A =/= C ) -> B =/= C ) $=
+    ( wceq wne neeq1 biimpd imp ) ABDZACEZBCEZIJKABCFGH $.
+
+  $( Obsolete version of ~ pm13.18 as of 14-May-2023.  (Contributed by Andrew
+     Salmon, 3-Jun-2011.)  (Proof modification is discouraged.)
+     (New usage is discouraged.) $)
+  pm13.18OLD $p |- ( ( A = B /\ A =/= C ) -> B =/= C ) $=
     ( wceq wne eqeq1 biimprd necon3d imp ) ABDZACEBCEJBCACJACDBCDABCFGHI $.
 
   $( Theorem *13.181 in [WhiteheadRussell] p. 178.  (Contributed by Andrew
@@ -27202,14 +27208,28 @@ choice between (what we call) a "definitional form" where the shorter
   $}
 
   $( Two classes are different if they don't contain the same element.
-     (Contributed by NM, 3-Feb-2012.) $)
+     (Contributed by NM, 3-Feb-2012.)  (Proof shortened by Wolf Lammen,
+     14-May-2023.) $)
   nelne1 $p |- ( ( A e. B /\ -. A e. C ) -> B =/= C ) $=
+    ( wcel wn wa nelneq2 neqned ) ABDACDEFBCABCGH $.
+
+  $( Obsolete version of ~ nelne1 asw of 14-May-2023.  (Contributed by NM,
+     3-Feb-2012.)  (Proof modification is discouraged.)
+     (New usage is discouraged.) $)
+  nelne1OLD $p |- ( ( A e. B /\ -. A e. C ) -> B =/= C ) $=
     ( wcel wn wne wceq eleq2 biimpcd necon3bd imp ) ABDZACDZEBCFLMBCBCGLMBCAHIJ
     K $.
 
   $( Two classes are different if they don't belong to the same class.
-     (Contributed by NM, 25-Jun-2012.) $)
+     (Contributed by NM, 25-Jun-2012.)  (Proof shortened by Wolf Lammen,
+     14-May-2023.) $)
   nelne2 $p |- ( ( A e. C /\ -. B e. C ) -> A =/= B ) $=
+    ( wcel wn wa nelneq neqned ) ACDBCDEFABABCGH $.
+
+  $( Obsolete version of ~ nelne2 asw of 14-May-2023.  (Contributed by NM,
+     25-Jun-2012.)  (Proof modification is discouraged.)
+     (New usage is discouraged.) $)
+  nelne2OLD $p |- ( ( A e. C /\ -. B e. C ) -> A =/= B ) $=
     ( wcel wn wne wceq eleq1 biimpcd necon3bd imp ) ACDZBCDZEABFLMABABGLMABCHIJ
     K $.