| Step |
Hyp |
Ref |
Expression |
| 1 |
|
5on |
Could not format 5o e. On : No typesetting found for |- 5o e. On with typecode |- |
| 2 |
|
sucidg |
Could not format ( 5o e. On -> 5o e. suc 5o ) : No typesetting found for |- ( 5o e. On -> 5o e. suc 5o ) with typecode |- |
| 3 |
1 2
|
ax-mp |
Could not format 5o e. suc 5o : No typesetting found for |- 5o e. suc 5o with typecode |- |
| 4 |
|
df-6o |
Could not format 6o = suc 5o : No typesetting found for |- 6o = suc 5o with typecode |- |
| 5 |
3 4
|
eleqtrri |
Could not format 5o e. 6o : No typesetting found for |- 5o e. 6o with typecode |- |
| 6 |
|
6olt9o |
Could not format 6o e. 9o : No typesetting found for |- 6o e. 9o with typecode |- |
| 7 |
|
9on |
Could not format 9o e. On : No typesetting found for |- 9o e. On with typecode |- |
| 8 |
|
ontr1 |
Could not format ( 9o e. On -> ( ( 5o e. 6o /\ 6o e. 9o ) -> 5o e. 9o ) ) : No typesetting found for |- ( 9o e. On -> ( ( 5o e. 6o /\ 6o e. 9o ) -> 5o e. 9o ) ) with typecode |- |
| 9 |
7 8
|
ax-mp |
Could not format ( ( 5o e. 6o /\ 6o e. 9o ) -> 5o e. 9o ) : No typesetting found for |- ( ( 5o e. 6o /\ 6o e. 9o ) -> 5o e. 9o ) with typecode |- |
| 10 |
5 6 9
|
mp2an |
Could not format 5o e. 9o : No typesetting found for |- 5o e. 9o with typecode |- |