Description: Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | dp2eq1i.1 | |- A = B |
|
Assertion | dp2eq1i | |- _ A C = _ B C |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dp2eq1i.1 | |- A = B |
|
2 | dp2eq1 | |- ( A = B -> _ A C = _ B C ) |
|
3 | 1 2 | ax-mp | |- _ A C = _ B C |