Metamath Proof Explorer

Theorem dp2eq2i

Description: Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015)

Ref Expression
Hypothesis dp2eq1i.1 
|- A = B
Assertion dp2eq2i 
|- _ C A = _ C B

Proof

Step Hyp Ref Expression
1 dp2eq1i.1 
 |-  A = B
2 dp2eq2 
 |-  ( A = B -> _ C A = _ C B )
3 1 2 ax-mp 
 |-  _ C A = _ C B