Theorem comraddi

Description: Commute RHS addition. See addcomli to commute addition on LHS. (Contributed by David A. Wheeler, 11-Oct-2018)

	Ref	Expression
Hypotheses	comraddi.1	⊢ 𝐵 ∈ ℂ
	comraddi.2	⊢ 𝐶 ∈ ℂ
	comraddi.3	⊢ 𝐴 = ( 𝐵 + 𝐶 )
Assertion	comraddi	⊢ 𝐴 = ( 𝐶 + 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		comraddi.1	⊢ 𝐵 ∈ ℂ
2		comraddi.2	⊢ 𝐶 ∈ ℂ
3		comraddi.3	⊢ 𝐴 = ( 𝐵 + 𝐶 )
4	1 2	addcomi	⊢ ( 𝐵 + 𝐶 ) = ( 𝐶 + 𝐵 )
5	3 4	eqtri	⊢ 𝐴 = ( 𝐶 + 𝐵 )