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

Metamath Proof Explorer

Theorem dp2eq2

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

Ref Expression
Assertion dp2eq2 Could not format assertion : No typesetting found for |- ( A = B -> _ C A = _ C B ) with typecode |-

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ A = B → A 10 = B 10
2 1 oveq2d ⊢ A = B → C + A 10 = C + B 10
3 df-dp2 Could not format _ C A = ( C + ( A / ; 1 0 ) ) : No typesetting found for |- _ C A = ( C + ( A / ; 1 0 ) ) with typecode |-
4 df-dp2 Could not format _ C B = ( C + ( B / ; 1 0 ) ) : No typesetting found for |- _ C B = ( C + ( B / ; 1 0 ) ) with typecode |-
5 2 3 4 3eqtr4g Could not format ( A = B -> _ C A = _ C B ) : No typesetting found for |- ( A = B -> _ C A = _ C B ) with typecode |-