Metamath Proof Explorer


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