Description: Any real number subtracted from itself forms a left additive identity. (Contributed by Steven Nguyen, 8-Jan-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | resubidaddid1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | readdsub | ||
2 | 1 | 3anidm13 | |
3 | repncan2 | ||
4 | 2 3 | eqtr3d |