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 | ||
reladdrsub.2 | |||
reladdrsub.3 | |||
Assertion | reladdrsub |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reladdrsub.1 | ||
2 | reladdrsub.2 | ||
3 | reladdrsub.3 | ||
4 | 1 2 | readdcld | |
5 | 3 4 | eqeltrrd | |
6 | resubadd | ||
7 | 3 6 | syl5ibrcom | |
8 | 5 1 2 7 | mp3and | |
9 | 8 | eqcomd |