Theorem decaddcom

Description: Commute ones place in addition. (Contributed by Steven Nguyen, 29-Jan-2023)

	Ref	Expression
Hypotheses	decaddcom.a	|- A e. NN0
	decaddcom.b	|- B e. NN0
	decaddcom.c	|- C e. NN0
Assertion	decaddcom	|- ( ; A B + C ) = ( ; A C + B )

Proof

Step	Hyp	Ref	Expression
1		decaddcom.a	|- A e. NN0
2		decaddcom.b	|- B e. NN0
3		decaddcom.c	|- C e. NN0
4		eqid	|- ; A B = ; A B
5		eqid	|- ( B + C ) = ( B + C )
6	1 2 3 4 5	decaddi	|- ( ; A B + C ) = ; A ( B + C )
7		eqid	|- ; A C = ; A C
8	3	nn0cni	|- C e. CC
9	2	nn0cni	|- B e. CC
10	8 9	addcomi	|- ( C + B ) = ( B + C )
11	1 3 2 7 10	decaddi	|- ( ; A C + B ) = ; A ( B + C )
12	6 11	eqtr4i	|- ( ; A B + C ) = ( ; A C + B )