Metamath Proof Explorer

Theorem deceq12i

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

Ref Expression
Hypotheses deceq1i.1 ⊢ 𝐴 = 𝐵
deceq12i.2 ⊢ 𝐶 = 𝐷
Assertion deceq12i 𝐴 𝐶 = 𝐵 𝐷

Proof

Step Hyp Ref Expression
1 deceq1i.1 ⊢ 𝐴 = 𝐵
2 deceq12i.2 ⊢ 𝐶 = 𝐷
3 1 deceq1i ⊢ 𝐴 𝐶 = 𝐵 𝐶
4 2 deceq2i ⊢ 𝐵 𝐶 = 𝐵 𝐷
5 3 4 eqtri ⊢ 𝐴 𝐶 = 𝐵 𝐷