Metamath Proof Explorer

Theorem deceq1i

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

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

Proof

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