Theorem deceq1i

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

	Ref	Expression
Hypothesis	deceq1i.1	$$⊢A=B$$
Assertion	deceq1i	Could not format assertion : No typesetting found for |- ; A C = ; B C with typecode |-

Proof

Step	Hyp	Ref	Expression
1		deceq1i.1	$$⊢A=B$$
2		deceq1	Could not format ( A = B -> ; A C = ; B C ) : No typesetting found for |- ( A = B -> ; A C = ; B C ) with typecode |-
3	1 2	ax-mp	Could not format ; A C = ; B C : No typesetting found for |- ; A C = ; B C with typecode |-