Description: Any translation belongs to the set of functions constructed for cdleme . TODO: Fix comment. (Contributed by NM, 22-Apr-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemg2.b | |
|
cdlemg2.l | |
||
cdlemg2.j | |
||
cdlemg2.m | |
||
cdlemg2.a | |
||
cdlemg2.h | |
||
cdlemg2.t | |
||
cdlemg2.u | |
||
cdlemg2.d | |
||
cdlemg2.e | |
||
cdlemg2.g | |
||
Assertion | cdlemg2cN | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemg2.b | |
|
2 | cdlemg2.l | |
|
3 | cdlemg2.j | |
|
4 | cdlemg2.m | |
|
5 | cdlemg2.a | |
|
6 | cdlemg2.h | |
|
7 | cdlemg2.t | |
|
8 | cdlemg2.u | |
|
9 | cdlemg2.d | |
|
10 | cdlemg2.e | |
|
11 | cdlemg2.g | |
|
12 | 2 5 6 7 | cdlemg1cN | |
13 | eqid | |
|
14 | 1 2 3 4 5 6 8 9 10 11 7 13 | cdlemg1b2 | |
15 | 14 | adantr | |
16 | 15 | eqeq2d | |
17 | 12 16 | bitrd | |