Theorem decaddcom

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

	Ref	Expression
Hypotheses	decaddcom.a	$$⊢A\in {\mathbb{N}}_0$$
	decaddcom.b	$$⊢B\in {\mathbb{N}}_0$$
	decaddcom.c	$$⊢C\in {\mathbb{N}}_0$$
Assertion	decaddcom	Could not format assertion : No typesetting found for |- ( ; A B + C ) = ( ; A C + B ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		decaddcom.a	$$⊢A\in {\mathbb{N}}_0$$
2		decaddcom.b	$$⊢B\in {\mathbb{N}}_0$$
3		decaddcom.c	$$⊢C\in {\mathbb{N}}_0$$
4		eqid	Could not format ; A B = ; A B : No typesetting found for |- ; A B = ; A B with typecode |-
5		eqid	$$⊢B+C=B+C$$
6	1 2 3 4 5	decaddi	Could not format ( ; A B + C ) = ; A ( B + C ) : No typesetting found for |- ( ; A B + C ) = ; A ( B + C ) with typecode |-
7		eqid	Could not format ; A C = ; A C : No typesetting found for |- ; A C = ; A C with typecode |-
8	3	nn0cni	$$⊢C\in ℂ$$
9	2	nn0cni	$$⊢B\in ℂ$$
10	8 9	addcomi	$$⊢C+B=B+C$$
11	1 3 2 7 10	decaddi	Could not format ( ; A C + B ) = ; A ( B + C ) : No typesetting found for |- ( ; A C + B ) = ; A ( B + C ) with typecode |-
12	6 11	eqtr4i	Could not format ( ; A B + C ) = ( ; A C + B ) : No typesetting found for |- ( ; A B + C ) = ( ; A C + B ) with typecode |-