Metamath Proof Explorer

Theorem dp2eq1

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

Ref Expression
Assertion dp2eq1 
|- ( A = B -> _ A C = _ B C )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( A = B -> ( A + ( C / ; 1 0 ) ) = ( B + ( C / ; 1 0 ) ) )
2 df-dp2 
 |-  _ A C = ( A + ( C / ; 1 0 ) )
3 df-dp2 
 |-  _ B C = ( B + ( C / ; 1 0 ) )
4 1 2 3 3eqtr4g 
 |-  ( A = B -> _ A C = _ B C )