Theorem dp2eq12i

Description: Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		dp2eq1i.1	$$⊢A=B$$
2		dp2eq12i.2	$$⊢C=D$$
3	1	dp2eq1i	Could not format _ A C = _ B C : No typesetting found for |- _ A C = _ B C with typecode |-
4	2	dp2eq2i	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 |-