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