Theorem bj-subcom

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

	Ref	Expression
Hypotheses	bj-subcom.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	bj-subcom.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
Assertion	bj-subcom	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) − ( 𝐵 · 𝐴 ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		bj-subcom.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		bj-subcom.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3	1 2	mulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℂ )
4	1 2	mulcomd	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
5	3 4	subeq0bd	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) − ( 𝐵 · 𝐴 ) ) = 0 )