add nadd32

metamath · Jan 21, 2025 · adaed15 · adaed15
1 parent 7e24b45
commit adaed15
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/set.mm b/set.mm
@@ -539980,6 +539980,14 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $=
       GVEVFVHDEFURUSYBVKUUIKYIGVEVFVHDEFUTUSVAVBVD $.
   $}
 
+  $( Commutative/associative law that swaps the last two terms in a triple
+     sum.  (Contributed by Scott Fenton, 20-Jan-2025.) $)
+  nadd32 $p |- ( ( A e. On /\ B e. On /\ C e. On ) ->
+  ( ( A +no B ) +no C ) = ( ( A +no C ) +no B ) ) $=
+    ( con0 wcel w3a cnadd co wceq naddcom 3adant1 oveq2d naddass 3com23 3eqtr4d
+    ) ADEZBDEZCDEZFZABCGHZGHACBGHZGHZABGHCGHACGHBGHZSTUAAGQRTUAIPBCJKLABCMPRQUC
+    UBIACBMNO $.
+
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   Surreal numbers - cuts and options