Description: Version of cdleme51finvtrN with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ltrniotaval.l | |
|
ltrniotaval.a | |
||
ltrniotaval.h | |
||
ltrniotaval.t | |
||
ltrniotaval.f | |
||
Assertion | ltrniotacnvN | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltrniotaval.l | |
|
2 | ltrniotaval.a | |
|
3 | ltrniotaval.h | |
|
4 | ltrniotaval.t | |
|
5 | ltrniotaval.f | |
|
6 | eqid | |
|
7 | eqid | |
|
8 | eqid | |
|
9 | eqid | |
|
10 | eqid | |
|
11 | eqid | |
|
12 | eqid | |
|
13 | 6 1 7 8 2 3 9 10 11 12 4 5 | cdlemg1finvtrlemN | |