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\to \frac{A}{10}=\frac{B}{10}$$
2	1	oveq2d	$$⊢A=B\to C+\left(\frac{A}{10}\right)=C+\left(\frac{B}{10}\right)$$
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 |-