Theorem naddassd

Description: Natural addition associates. 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	naddassd	|- ( ph -> ( ( A +no B ) +no C ) = ( A +no ( B +no C ) ) )

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		naddass	|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = ( A +no ( B +no C ) ) )
5	1 2 3 4	syl3anc	|- ( ph -> ( ( A +no B ) +no C ) = ( A +no ( B +no C ) ) )