Theorem deceq2i

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

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

Proof

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