Metamath Proof Explorer


Theorem resubsub4

Description: Law for double subtraction. Compare subsub4 . (Contributed by Steven Nguyen, 14-Jan-2023)

Ref Expression
Assertion resubsub4 A B C A - B - C = A - B + C

Proof

Step Hyp Ref Expression
1 readdcl B C B + C
2 1 3adant1 A B C B + C
3 rersubcl A B A - B
4 3 3adant3 A B C A - B
5 simp3 A B C C
6 rersubcl A - B C A - B - C
7 4 5 6 syl2anc A B C A - B - C
8 simp2 A B C B
9 8 recnd A B C B
10 5 recnd A B C C
11 7 recnd A B C A - B - C
12 9 10 11 addassd A B C B + C + A - B - C = B + C + A - B - C
13 repncan3 C A - B C + A - B - C = A - B
14 5 4 13 syl2anc A B C C + A - B - C = A - B
15 14 oveq2d A B C B + C + A - B - C = B + A - B
16 simp1 A B C A
17 repncan3 B A B + A - B = A
18 8 16 17 syl2anc A B C B + A - B = A
19 12 15 18 3eqtrd A B C B + C + A - B - C = A
20 2 7 19 reladdrsub A B C A - B - C = A - B + C