Metamath Proof Explorer


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 φ A
reladdrsub.2 φ B
reladdrsub.3 φ A + B = C
Assertion reladdrsub φ B = C - A

Proof

Step Hyp Ref Expression
1 reladdrsub.1 φ A
2 reladdrsub.2 φ B
3 reladdrsub.3 φ A + B = C
4 1 2 readdcld φ A + B
5 3 4 eqeltrrd φ C
6 resubadd C A B C - A = B A + B = C
7 3 6 syl5ibrcom φ C A B C - A = B
8 5 1 2 7 mp3and φ C - A = B
9 8 eqcomd φ B = C - A