Description: The three place congruence predicate. This is an abbreviation for saying that all three pair in a triple are congruent with each other. Three place form of Definition 4.4 of Schwabhauser p. 35. (Contributed by Scott Fenton, 4-Oct-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | df-cgr3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | ccgr3 | |
|
1 | vp | |
|
2 | vq | |
|
3 | vn | |
|
4 | cn | |
|
5 | va | |
|
6 | cee | |
|
7 | 3 | cv | |
8 | 7 6 | cfv | |
9 | vb | |
|
10 | vc | |
|
11 | vd | |
|
12 | ve | |
|
13 | vf | |
|
14 | 1 | cv | |
15 | 5 | cv | |
16 | 9 | cv | |
17 | 10 | cv | |
18 | 16 17 | cop | |
19 | 15 18 | cop | |
20 | 14 19 | wceq | |
21 | 2 | cv | |
22 | 11 | cv | |
23 | 12 | cv | |
24 | 13 | cv | |
25 | 23 24 | cop | |
26 | 22 25 | cop | |
27 | 21 26 | wceq | |
28 | 15 16 | cop | |
29 | ccgr | |
|
30 | 22 23 | cop | |
31 | 28 30 29 | wbr | |
32 | 15 17 | cop | |
33 | 22 24 | cop | |
34 | 32 33 29 | wbr | |
35 | 18 25 29 | wbr | |
36 | 31 34 35 | w3a | |
37 | 20 27 36 | w3a | |
38 | 37 13 8 | wrex | |
39 | 38 12 8 | wrex | |
40 | 39 11 8 | wrex | |
41 | 40 10 8 | wrex | |
42 | 41 9 8 | wrex | |
43 | 42 5 8 | wrex | |
44 | 43 3 4 | wrex | |
45 | 44 1 2 | copab | |
46 | 0 45 | wceq | |