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