Theorem bj-subcom

Description: A consequence of commutativity of multiplication. (Contributed by BJ, 6-Jun-2019)

	Ref	Expression
Hypotheses	bj-subcom.a	|- ( ph -> A e. CC )
	bj-subcom.b	|- ( ph -> B e. CC )
Assertion	bj-subcom	|- ( ph -> ( ( A x. B ) - ( B x. A ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		bj-subcom.a	|- ( ph -> A e. CC )
2		bj-subcom.b	|- ( ph -> B e. CC )
3	1 2	mulcld	|- ( ph -> ( A x. B ) e. CC )
4	1 2	mulcomd	|- ( ph -> ( A x. B ) = ( B x. A ) )
5	3 4	subeq0bd	|- ( ph -> ( ( A x. B ) - ( B x. A ) ) = 0 )