Metamath Proof Explorer


Theorem resubidaddid1lem

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

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

Proof

Step Hyp Ref Expression
1 resubidaddid1lem.a φ A
2 resubidaddid1lem.b φ B
3 resubidaddid1lem.c φ C
4 resubidaddid1lem.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