Theorem addcomgi

Description: Generalization of commutative law for addition. Simplifies proofs dealing with vectors. However, it is dependent on our particular definition of ordered pair. (Contributed by Andrew Salmon, 28-Jan-2012) (Revised by Mario Carneiro, 6-May-2015)

	Ref	Expression
Assertion	addcomgi	|- ( A + B ) = ( B + A )

Proof

Step	Hyp	Ref	Expression
1		addcom	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
2		ax-addf	|- + : ( CC X. CC ) --> CC
3	2	fdmi	|- dom + = ( CC X. CC )
4	3	ndmovcom	|- ( -. ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
5	1 4	pm2.61i	|- ( A + B ) = ( B + A )