Theorem mvrrsubd

Description: Move a subtraction in the RHS to a right-addition in the LHS. Converse of mvlraddd .

EDITORIAL: Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024)

	Ref	Expression
Hypotheses	mvrrsubd.a	$$⊢\phi \to B\in ℂ$$
	mvrrsubd.b	$$⊢\phi \to C\in ℂ$$
	mvrrsubd.1	$$⊢\phi \to A=B-C$$
Assertion	mvrrsubd	$$⊢\phi \to A+C=B$$

Proof

Step	Hyp	Ref	Expression
1		mvrrsubd.a	$$⊢\phi \to B\in ℂ$$
2		mvrrsubd.b	$$⊢\phi \to C\in ℂ$$
3		mvrrsubd.1	$$⊢\phi \to A=B-C$$
4	1 2	subcld	$$⊢\phi \to B-C\in ℂ$$
5	3 4	eqeltrd	$$⊢\phi \to A\in ℂ$$
6	5 2	addcld	$$⊢\phi \to A+C\in ℂ$$
7	5 2	pncand	$$⊢\phi \to A+C-C=A$$
8	7 3	eqtrd	$$⊢\phi \to A+C-C=B-C$$
9	6 1 2 8	subcan2d	$$⊢\phi \to A+C=B$$