Metamath Proof Explorer

Theorem deceq12i

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

Ref Expression
Hypotheses deceq1i.1 
|- A = B
deceq12i.2 
|- C = D
Assertion deceq12i 
|- ; A C = ; B D

Proof

Step Hyp Ref Expression
1 deceq1i.1 
 |-  A = B
2 deceq12i.2 
 |-  C = D
3 1 deceq1i 
 |-  ; A C = ; B C
4 2 deceq2i 
 |-  ; B C = ; B D
5 3 4 eqtri 
 |-  ; A C = ; B D