Detailed syntax breakdown of Definition df-qpOLD
Step | Hyp | Ref
| Expression |
1 | | cqpOLD 31544 |
. 2
QpOLD |
2 | | vp |
. . 3
|
3 | | cprime 15385 |
. . 3
|
4 | | vb |
. . . 4
|
5 | | vh |
. . . . . . . . . 10
|
6 | 5 | cv 1482 |
. . . . . . . . 9
|
7 | 6 | ccnv 5113 |
. . . . . . . 8
|
8 | | cz 11377 |
. . . . . . . . 9
|
9 | | cc0 9936 |
. . . . . . . . . 10
|
10 | 9 | csn 4177 |
. . . . . . . . 9
|
11 | 8, 10 | cdif 3571 |
. . . . . . . 8
|
12 | 7, 11 | cima 5117 |
. . . . . . 7
|
13 | | vx |
. . . . . . . 8
|
14 | 13 | cv 1482 |
. . . . . . 7
|
15 | 12, 14 | wss 3574 |
. . . . . 6
|
16 | | cuz 11687 |
. . . . . . 7
|
17 | 16 | crn 5115 |
. . . . . 6
|
18 | 15, 13, 17 | wrex 2913 |
. . . . 5
|
19 | 2 | cv 1482 |
. . . . . . . 8
|
20 | | c1 9937 |
. . . . . . . 8
|
21 | | cmin 10266 |
. . . . . . . 8
|
22 | 19, 20, 21 | co 6650 |
. . . . . . 7
|
23 | | cfz 12326 |
. . . . . . 7
|
24 | 9, 22, 23 | co 6650 |
. . . . . 6
|
25 | | cmap 7857 |
. . . . . 6
|
26 | 8, 24, 25 | co 6650 |
. . . . 5
|
27 | 18, 5, 26 | crab 2916 |
. . . 4
|
28 | | cnx 15854 |
. . . . . . . . 9
|
29 | | cbs 15857 |
. . . . . . . . 9
|
30 | 28, 29 | cfv 5888 |
. . . . . . . 8
|
31 | 4 | cv 1482 |
. . . . . . . 8
|
32 | 30, 31 | cop 4183 |
. . . . . . 7
|
33 | | cplusg 15941 |
. . . . . . . . 9
|
34 | 28, 33 | cfv 5888 |
. . . . . . . 8
|
35 | | vf |
. . . . . . . . 9
|
36 | | vg |
. . . . . . . . 9
|
37 | 35 | cv 1482 |
. . . . . . . . . . 11
|
38 | 36 | cv 1482 |
. . . . . . . . . . 11
|
39 | | caddc 9939 |
. . . . . . . . . . . 12
|
40 | 39 | cof 6895 |
. . . . . . . . . . 11
|
41 | 37, 38, 40 | co 6650 |
. . . . . . . . . 10
|
42 | | crqp 31542 |
. . . . . . . . . . 11
/Qp |
43 | 19, 42 | cfv 5888 |
. . . . . . . . . 10
/Qp |
44 | 41, 43 | cfv 5888 |
. . . . . . . . 9
/Qp |
45 | 35, 36, 31, 31, 44 | cmpt2 6652 |
. . . . . . . 8
/Qp |
46 | 34, 45 | cop 4183 |
. . . . . . 7
/Qp
|
47 | | cmulr 15942 |
. . . . . . . . 9
|
48 | 28, 47 | cfv 5888 |
. . . . . . . 8
|
49 | | vn |
. . . . . . . . . . 11
|
50 | | vk |
. . . . . . . . . . . . . . 15
|
51 | 50 | cv 1482 |
. . . . . . . . . . . . . 14
|
52 | 51, 37 | cfv 5888 |
. . . . . . . . . . . . 13
|
53 | 49 | cv 1482 |
. . . . . . . . . . . . . . 15
|
54 | 53, 51, 21 | co 6650 |
. . . . . . . . . . . . . 14
|
55 | 54, 38 | cfv 5888 |
. . . . . . . . . . . . 13
|
56 | | cmul 9941 |
. . . . . . . . . . . . 13
|
57 | 52, 55, 56 | co 6650 |
. . . . . . . . . . . 12
|
58 | 8, 57, 50 | csu 14416 |
. . . . . . . . . . 11
|
59 | 49, 8, 58 | cmpt 4729 |
. . . . . . . . . 10
|
60 | 59, 43 | cfv 5888 |
. . . . . . . . 9
/Qp
|
61 | 35, 36, 31, 31, 60 | cmpt2 6652 |
. . . . . . . 8
/Qp
|
62 | 48, 61 | cop 4183 |
. . . . . . 7
/Qp |
63 | 32, 46, 62 | ctp 4181 |
. . . . . 6
/Qp
/Qp
|
64 | | cple 15948 |
. . . . . . . . 9
|
65 | 28, 64 | cfv 5888 |
. . . . . . . 8
|
66 | 37, 38 | cpr 4179 |
. . . . . . . . . . 11
|
67 | 66, 31 | wss 3574 |
. . . . . . . . . 10
|
68 | 51 | cneg 10267 |
. . . . . . . . . . . . . 14
|
69 | 68, 37 | cfv 5888 |
. . . . . . . . . . . . 13
|
70 | 19, 20, 39 | co 6650 |
. . . . . . . . . . . . . 14
|
71 | | cexp 12860 |
. . . . . . . . . . . . . 14
|
72 | 70, 68, 71 | co 6650 |
. . . . . . . . . . . . 13
|
73 | 69, 72, 56 | co 6650 |
. . . . . . . . . . . 12
|
74 | 8, 73, 50 | csu 14416 |
. . . . . . . . . . 11
|
75 | 68, 38 | cfv 5888 |
. . . . . . . . . . . . 13
|
76 | 75, 72, 56 | co 6650 |
. . . . . . . . . . . 12
|
77 | 8, 76, 50 | csu 14416 |
. . . . . . . . . . 11
|
78 | | clt 10074 |
. . . . . . . . . . 11
|
79 | 74, 77, 78 | wbr 4653 |
. . . . . . . . . 10
|
80 | 67, 79 | wa 384 |
. . . . . . . . 9
|
81 | 80, 35, 36 | copab 4712 |
. . . . . . . 8
|
82 | 65, 81 | cop 4183 |
. . . . . . 7
|
83 | 82 | csn 4177 |
. . . . . 6
|
84 | 63, 83 | cun 3572 |
. . . . 5
/Qp
/Qp
|
85 | 8, 10 | cxp 5112 |
. . . . . . . 8
|
86 | 37, 85 | wceq 1483 |
. . . . . . 7
|
87 | 37 | ccnv 5113 |
. . . . . . . . . . 11
|
88 | 87, 11 | cima 5117 |
. . . . . . . . . 10
|
89 | | cr 9935 |
. . . . . . . . . 10
|
90 | 78 | ccnv 5113 |
. . . . . . . . . 10
|
91 | 88, 89, 90 | csup 8346 |
. . . . . . . . 9
|
92 | 91 | cneg 10267 |
. . . . . . . 8
|
93 | 19, 92, 71 | co 6650 |
. . . . . . 7
|
94 | 86, 9, 93 | cif 4086 |
. . . . . 6
|
95 | 35, 31, 94 | cmpt 4729 |
. . . . 5
|
96 | | ctng 22383 |
. . . . 5
toNrmGrp |
97 | 84, 95, 96 | co 6650 |
. . . 4
/Qp
/Qp
toNrmGrp |
98 | 4, 27, 97 | csb 3533 |
. . 3
/Qp
/Qp
toNrmGrp |
99 | 2, 3, 98 | cmpt 4729 |
. 2
/Qp
/Qp
toNrmGrp |
100 | 1, 99 | wceq 1483 |
1
QpOLD /Qp
/Qp
toNrmGrp |