Metamath Proof Explorer

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	$⊢ φ \to A \in On$
	nadd.2	$⊢ φ \to B \in On$
	nadd.3	$⊢ φ \to C \in On$
Assertion	nadd32d	$⊢ φ \to (A + B) + C = (A + C) + B$

Proof

Step	Hyp	Ref	Expression
1		nadd.1	$⊢ φ \to A \in On$
2		nadd.2	$⊢ φ \to B \in On$
3		nadd.3	$⊢ φ \to C \in On$
4		nadd32	$⊢ (A \in On \land B \in On \land C \in On) \to (A + B) + C = (A + C) + B$
5	1 2 3 4	syl3anc	$⊢ φ \to (A + B) + C = (A + C) + B$