This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dp2eq1i

Description: Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015)

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

Proof

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