Theorem reladdrsub

Description: Move LHS of a sum into RHS of a (real) difference. Version of mvlladdd with real subtraction. (Contributed by Steven Nguyen, 8-Jan-2023)

	Ref	Expression
Hypotheses	reladdrsub.1	$$⊢\phi \to A\in ℝ$$
	reladdrsub.2	$$⊢\phi \to B\in ℝ$$
	reladdrsub.3	$$⊢\phi \to A+B=C$$
Assertion	reladdrsub	$$⊢\phi \to B=C{-}_{ℝ}A$$

Proof

Step	Hyp	Ref	Expression
1		reladdrsub.1	$$⊢\phi \to A\in ℝ$$
2		reladdrsub.2	$$⊢\phi \to B\in ℝ$$
3		reladdrsub.3	$$⊢\phi \to A+B=C$$
4	1 2	readdcld	$$⊢\phi \to A+B\in ℝ$$
5	3 4	eqeltrrd	$$⊢\phi \to C\in ℝ$$
6		resubadd	$$⊢\left(C\in ℝ\wedge A\in ℝ\wedge B\in ℝ\right)\to \left(C{-}_{ℝ}A=B\leftrightarrow A+B=C\right)$$
7	3 6	syl5ibrcom	$$⊢\phi \to \left(\left(C\in ℝ\wedge A\in ℝ\wedge B\in ℝ\right)\to C{-}_{ℝ}A=B\right)$$
8	5 1 2 7	mp3and	$$⊢\phi \to C{-}_{ℝ}A=B$$
9	8	eqcomd	$$⊢\phi \to B=C{-}_{ℝ}A$$