Metamath Proof Explorer


Theorem dp2eq1i

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

Proof

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