Metamath Proof Explorer


Theorem resubcan2

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

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

Proof

Step Hyp Ref Expression
1 simpr A B C A - C = B - C A - C = B - C
2 simpl1 A B C A - C = B - C A
3 simpl3 A B C A - C = B - C C
4 simpl2 A B C A - C = B - C B
5 rersubcl B C B - C
6 4 3 5 syl2anc A B C A - C = B - C B - C
7 2 3 6 resubaddd A B C A - C = B - C A - C = B - C C + B - C = A
8 1 7 mpbid A B C A - C = B - C C + B - C = A
9 repncan3 C B C + B - C = B
10 3 4 9 syl2anc A B C A - C = B - C C + B - C = B
11 8 10 eqtr3d A B C A - C = B - C A = B
12 11 ex A B C A - C = B - C A = B
13 oveq1 A = B A - C = B - C
14 12 13 impbid1 A B C A - C = B - C A = B