Theorem deceq12i

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

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

Proof

Step	Hyp	Ref	Expression
1		deceq1i.1	$$⊢A=B$$
2		deceq12i.2	$$⊢C=D$$
3	1	deceq1i	Could not format ; A C = ; B C : No typesetting found for |- ; A C = ; B C with typecode |-
4	2	deceq2i	Could not format ; B C = ; B D : No typesetting found for |- ; B C = ; B D with typecode |-
5	3 4	eqtri	Could not format ; A C = ; B D : No typesetting found for |- ; A C = ; B D with typecode |-