Metamath Proof Explorer

Theorem deceq2i

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

Ref Expression
Hypothesis deceq1i.1 ⊢ 𝐴 = 𝐵
Assertion deceq2i 𝐶 𝐴 = 𝐶 𝐵

Proof

Step Hyp Ref Expression
1 deceq1i.1 ⊢ 𝐴 = 𝐵
2 deceq2 ⊢ ( 𝐴 = 𝐵 → 𝐶 𝐴 = 𝐶 𝐵 )
3 1 2 ax-mp ⊢ 𝐶 𝐴 = 𝐶 𝐵