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 𝐴 𝐶 = 𝐵 𝐶