Theorem mvlraddi

Description: Move the right term in a sum on the LHS to the RHS. (Contributed by David A. Wheeler, 11-Oct-2018)

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

Proof

Step	Hyp	Ref	Expression
1		mvlraddi.1	|- A e. CC
2		mvlraddi.2	|- B e. CC
3		mvlraddi.3	|- ( A + B ) = C
4	1 2	pncan3oi	|- ( ( A + B ) - B ) = A
5	3	oveq1i	|- ( ( A + B ) - B ) = ( C - B )
6	4 5	eqtr3i	|- A = ( C - B )