Step |
Hyp |
Ref |
Expression |
1 |
|
dplt.a |
|
2 |
|
dplt.b |
|
3 |
|
dplt.d |
|
4 |
|
dplt.1 |
|
5 |
1 2 3 4
|
dp2lt |
Could not format _ A B < _ A C : No typesetting found for |- _ A B < _ A C with typecode |- |
6 |
1 2
|
dpval3rp |
Could not format ( A . B ) = _ A B : No typesetting found for |- ( A . B ) = _ A B with typecode |- |
7 |
1 3
|
dpval3rp |
Could not format ( A . C ) = _ A C : No typesetting found for |- ( A . C ) = _ A C with typecode |- |
8 |
5 6 7
|
3brtr4i |
|