Theorem laddrotrd

Description: Rotate the variables right in an equation with addition on the left, converting it into a subtraction. Version of mvlladdd with a commuted consequent, and of mvrladdd with a commuted hypothesis.

EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: ply1dg3rt0irred . (Contributed by SN, 21-Aug-2024)

	Ref	Expression
Hypotheses	laddrotrd.a	|- ( ph -> A e. CC )
	laddrotrd.b	|- ( ph -> B e. CC )
	laddrotrd.1	|- ( ph -> ( A + B ) = C )
Assertion	laddrotrd	|- ( ph -> ( C - A ) = B )

Proof

Step	Hyp	Ref	Expression
1		laddrotrd.a	|- ( ph -> A e. CC )
2		laddrotrd.b	|- ( ph -> B e. CC )
3		laddrotrd.1	|- ( ph -> ( A + B ) = C )
4	1 2 3	mvlladdd	|- ( ph -> B = ( C - A ) )
5	4	eqcomd	|- ( ph -> ( C - A ) = B )