Theorem nadd32

Description: Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by Scott Fenton, 20-Jan-2025)

	Ref	Expression
Assertion	nadd32	Could not format assertion : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = ( ( A +no C ) +no B ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		naddcom	Could not format ( ( B e. On /\ C e. On ) -> ( B +no C ) = ( C +no B ) ) : No typesetting found for |- ( ( B e. On /\ C e. On ) -> ( B +no C ) = ( C +no B ) ) with typecode |-
2	1	3adant1	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( B +no C ) = ( C +no B ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( B +no C ) = ( C +no B ) ) with typecode |-
3	2	oveq2d	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( A +no ( B +no C ) ) = ( A +no ( C +no B ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A +no ( B +no C ) ) = ( A +no ( C +no B ) ) ) with typecode |-
4		naddass	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = ( A +no ( B +no C ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = ( A +no ( B +no C ) ) ) with typecode |-
5		naddass	Could not format ( ( A e. On /\ C e. On /\ B e. On ) -> ( ( A +no C ) +no B ) = ( A +no ( C +no B ) ) ) : No typesetting found for |- ( ( A e. On /\ C e. On /\ B e. On ) -> ( ( A +no C ) +no B ) = ( A +no ( C +no B ) ) ) with typecode |-
6	5	3com23	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no C ) +no B ) = ( A +no ( C +no B ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no C ) +no B ) = ( A +no ( C +no B ) ) ) with typecode |-
7	3 4 6	3eqtr4d	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = ( ( A +no C ) +no B ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = ( ( A +no C ) +no B ) ) with typecode |-