Description: Any function of the form of the function constructed for cdleme is a translation. TODO: Fix comment. (Contributed by NM, 18-Apr-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemg1c.l | |
|
cdlemg1c.a | |
||
cdlemg1c.h | |
||
cdlemg1c.t | |
||
Assertion | cdlemg1ci2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemg1c.l | |
|
2 | cdlemg1c.a | |
|
3 | cdlemg1c.h | |
|
4 | cdlemg1c.t | |
|
5 | simpr | |
|
6 | eqid | |
|
7 | 1 2 3 4 6 | ltrniotacl | |
8 | 7 | adantr | |
9 | 5 8 | eqeltrd | |