Metamath Proof Explorer


Theorem rennncan2

Description: Cancellation law for real subtraction. Compare nnncan2 . (Contributed by Steven Nguyen, 14-Jan-2023)

Ref Expression
Assertion rennncan2 A B C A - C - B - C = A - B

Proof

Step Hyp Ref Expression
1 simp1 A B C A
2 simp3 A B C C
3 simp2 A B C B
4 rersubcl B C B - C
5 3 2 4 syl2anc A B C B - C
6 resubsub4 A C B - C A - C - B - C = A - C + B - C
7 1 2 5 6 syl3anc A B C A - C - B - C = A - C + B - C
8 repncan3 C B C + B - C = B
9 2 3 8 syl2anc A B C C + B - C = B
10 9 oveq2d A B C A - C + B - C = A - B
11 7 10 eqtrd A B C A - C - B - C = A - B