Metamath Proof Explorer

Theorem deceq2

Description: Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015) (Revised by AV, 6-Sep-2021)

Ref Expression
Assertion deceq2 
|- ( A = B -> ; C A = ; C B )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( A = B -> ( ( ( 9 + 1 ) x. C ) + A ) = ( ( ( 9 + 1 ) x. C ) + B ) )
2 df-dec 
 |-  ; C A = ( ( ( 9 + 1 ) x. C ) + A )
3 df-dec 
 |-  ; C B = ( ( ( 9 + 1 ) x. C ) + B )
4 1 2 3 3eqtr4g 
 |-  ( A = B -> ; C A = ; C B )