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

Metamath Proof Explorer

Theorem dp2eq12i

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

Ref Expression
Hypotheses dp2eq1i.1 
|- A = B
dp2eq12i.2 
|- C = D
Assertion dp2eq12i 
|- _ A C = _ B D

Proof

Step Hyp Ref Expression
1 dp2eq1i.1 
 |-  A = B
2 dp2eq12i.2 
 |-  C = D
3 1 dp2eq1i 
 |-  _ A C = _ B C
4 2 dp2eq2i 
 |-  _ B C = _ B D
5 3 4 eqtri 
 |-  _ A C = _ B D