Theorem comraddd

Description: Commute RHS addition, in deduction form. (Contributed by David A. Wheeler, 11-Oct-2018)

	Ref	Expression
Hypotheses	comraddd.1	|- ( ph -> B e. CC )
	comraddd.2	|- ( ph -> C e. CC )
	comraddd.3	|- ( ph -> A = ( B + C ) )
Assertion	comraddd	|- ( ph -> A = ( C + B ) )

Proof

Step	Hyp	Ref	Expression
1		comraddd.1	|- ( ph -> B e. CC )
2		comraddd.2	|- ( ph -> C e. CC )
3		comraddd.3	|- ( ph -> A = ( B + C ) )
4	1 2	addcomd	|- ( ph -> ( B + C ) = ( C + B ) )
5	3 4	eqtrd	|- ( ph -> A = ( C + B ) )