Description: Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | deceq1i.1 | ||
deceq12i.2 | |||
Assertion | deceq12i | Could not format assertion : No typesetting found for |- ; A C = ; B D with typecode |- |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | deceq1i.1 | ||
2 | deceq12i.2 | ||
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 |- |