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

Metamath Proof Explorer

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 \|-

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 \|-