Metamath Proof Explorer


Theorem repncan2

Description: Addition and subtraction of equals. Compare pncan2 . (Contributed by Steven Nguyen, 8-Jan-2023)

Ref Expression
Assertion repncan2 A B A + B - A = B

Proof

Step Hyp Ref Expression
1 eqid A + B = A + B
2 readdcl A B A + B
3 simpl A B A
4 simpr A B B
5 2 3 4 resubaddd A B A + B - A = B A + B = A + B
6 1 5 mpbiri A B A + B - A = B