Metamath Proof Explorer


Theorem resubidaddlidlem

Description: Lemma for resubidaddlid . A special case of npncan . (Contributed by Steven Nguyen, 8-Jan-2023)

Ref Expression
Hypotheses resubidaddridlem.a φ A
resubidaddridlem.b φ B
resubidaddridlem.c φ C
resubidaddridlem.1 φ A - B = B - C
Assertion resubidaddlidlem φ A - B + B - C = A - C

Proof

Step Hyp Ref Expression
1 resubidaddridlem.a φ A
2 resubidaddridlem.b φ B
3 resubidaddridlem.c φ C
4 resubidaddridlem.1 φ A - B = B - C
5 rersubcl A B A - B
6 1 2 5 syl2anc φ A - B
7 rersubcl B C B - C
8 2 3 7 syl2anc φ B - C
9 6 8 readdcld φ A - B + B - C
10 4 eqcomd φ B - C = A - B
11 2 3 6 resubaddd φ B - C = A - B C + A - B = B
12 10 11 mpbid φ C + A - B = B
13 12 oveq1d φ C + A - B + B - C = B + B - C
14 3 recnd φ C
15 6 recnd φ A - B
16 8 recnd φ B - C
17 14 15 16 addassd φ C + A - B + B - C = C + A - B + B - C
18 1 2 8 resubaddd φ A - B = B - C B + B - C = A
19 4 18 mpbid φ B + B - C = A
20 13 17 19 3eqtr3d φ C + A - B + B - C = A
21 3 9 20 reladdrsub φ A - B + B - C = A - C