Metamath Proof Explorer


Theorem reppncan

Description: Cancellation law for mixed addition and real subtraction. Compare ppncan . (Contributed by SN, 3-Sep-2023)

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

Proof

Step Hyp Ref Expression
1 repnpcan A B C A + B - A + C = B - C
2 readdcl A B A + B
3 2 3adant3 A B C A + B
4 readdcl A C A + C
5 4 3adant2 A B C A + C
6 rersubcl B C B - C
7 6 3adant1 A B C B - C
8 3 5 7 resubaddd A B C A + B - A + C = B - C A + C + B - C = A + B
9 1 8 mpbid A B C A + C + B - C = A + B