Theorem nadd32d

Description: Commutative/associative law that swaps the last two terms in a triple sum. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026)

	Ref	Expression
Hypotheses	nadd.1	|- ( ph -> A e. On )
	nadd.2	|- ( ph -> B e. On )
	nadd.3	|- ( ph -> C e. On )
Assertion	nadd32d	|- ( ph -> ( ( A +no B ) +no C ) = ( ( A +no C ) +no B ) )

Proof

Step	Hyp	Ref	Expression
1		nadd.1	|- ( ph -> A e. On )
2		nadd.2	|- ( ph -> B e. On )
3		nadd.3	|- ( ph -> C e. On )
4		nadd32	|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = ( ( A +no C ) +no B ) )
5	1 2 3 4	syl3anc	|- ( ph -> ( ( A +no B ) +no C ) = ( ( A +no C ) +no B ) )