Metamath Proof Explorer


Theorem resubidaddid1

Description: Any real number subtracted from itself forms a left additive identity. (Contributed by Steven Nguyen, 8-Jan-2023)

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

Proof

Step Hyp Ref Expression
1 readdsub A B A A + B - A = A - A + B
2 1 3anidm13 A B A + B - A = A - A + B
3 repncan2 A B A + B - A = B
4 2 3 eqtr3d A B A - A + B = B