Theorem bj-subcom

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

	Ref	Expression
Hypotheses	bj-subcom.a	$$⊢\phi \to A\in ℂ$$
	bj-subcom.b	$$⊢\phi \to B\in ℂ$$
Assertion	bj-subcom	$$⊢\phi \to AB-BA=0$$

Proof

Step	Hyp	Ref	Expression
1		bj-subcom.a	$$⊢\phi \to A\in ℂ$$
2		bj-subcom.b	$$⊢\phi \to B\in ℂ$$
3	1 2	mulcld	$$⊢\phi \to AB\in ℂ$$
4	1 2	mulcomd	$$⊢\phi \to AB=BA$$
5	3 4	subeq0bd	$$⊢\phi \to AB-BA=0$$