This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dp2eq2i

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

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

Step	Hyp	Ref	Expression
1		dp2eq1i.1	$⊢ A = B$
2		dp2eq2	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 \|-