Theorem deceq1

Description: Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015) (Revised by AV, 6-Sep-2021)

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢A=B\to \left(9+1\right)A=\left(9+1\right)B$$
2	1	oveq1d	$$⊢A=B\to \left(9+1\right)A+C=\left(9+1\right)B+C$$
3		df-dec	Could not format ; A C = ( ( ( 9 + 1 ) x. A ) + C ) : No typesetting found for |- ; A C = ( ( ( 9 + 1 ) x. A ) + C ) with typecode |-
4		df-dec	Could not format ; B C = ( ( ( 9 + 1 ) x. B ) + C ) : No typesetting found for |- ; B C = ( ( ( 9 + 1 ) x. B ) + C ) with typecode |-
5	2 3 4	3eqtr4g	Could not format ( A = B -> ; A C = ; B C ) : No typesetting found for |- ( A = B -> ; A C = ; B C ) with typecode |-