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