Step |
Hyp |
Ref |
Expression |
0 |
|
cconstr |
|
1 |
|
vs |
|
2 |
|
cvv |
|
3 |
|
vx |
|
4 |
|
cc |
|
5 |
|
va |
|
6 |
1
|
cv |
|
7 |
|
vb |
|
8 |
|
vc |
|
9 |
|
vd |
|
10 |
|
vt |
|
11 |
|
cr |
|
12 |
|
vr |
|
13 |
3
|
cv |
|
14 |
5
|
cv |
|
15 |
|
caddc |
|
16 |
10
|
cv |
|
17 |
|
cmul |
|
18 |
7
|
cv |
|
19 |
|
cmin |
|
20 |
18 14 19
|
co |
|
21 |
16 20 17
|
co |
|
22 |
14 21 15
|
co |
|
23 |
13 22
|
wceq |
|
24 |
8
|
cv |
|
25 |
12
|
cv |
|
26 |
9
|
cv |
|
27 |
26 24 19
|
co |
|
28 |
25 27 17
|
co |
|
29 |
24 28 15
|
co |
|
30 |
13 29
|
wceq |
|
31 |
|
cim |
|
32 |
|
ccj |
|
33 |
20 32
|
cfv |
|
34 |
33 27 17
|
co |
|
35 |
34 31
|
cfv |
|
36 |
|
cc0 |
|
37 |
35 36
|
wne |
|
38 |
23 30 37
|
w3a |
|
39 |
38 12 11
|
wrex |
|
40 |
39 10 11
|
wrex |
|
41 |
40 9 6
|
wrex |
|
42 |
41 8 6
|
wrex |
|
43 |
42 7 6
|
wrex |
|
44 |
43 5 6
|
wrex |
|
45 |
|
ve |
|
46 |
|
vf |
|
47 |
|
cabs |
|
48 |
13 24 19
|
co |
|
49 |
48 47
|
cfv |
|
50 |
45
|
cv |
|
51 |
46
|
cv |
|
52 |
50 51 19
|
co |
|
53 |
52 47
|
cfv |
|
54 |
49 53
|
wceq |
|
55 |
23 54
|
wa |
|
56 |
55 10 11
|
wrex |
|
57 |
56 46 6
|
wrex |
|
58 |
57 45 6
|
wrex |
|
59 |
58 8 6
|
wrex |
|
60 |
59 7 6
|
wrex |
|
61 |
60 5 6
|
wrex |
|
62 |
14 26
|
wne |
|
63 |
13 14 19
|
co |
|
64 |
63 47
|
cfv |
|
65 |
18 24 19
|
co |
|
66 |
65 47
|
cfv |
|
67 |
64 66
|
wceq |
|
68 |
13 26 19
|
co |
|
69 |
68 47
|
cfv |
|
70 |
69 53
|
wceq |
|
71 |
62 67 70
|
w3a |
|
72 |
71 46 6
|
wrex |
|
73 |
72 45 6
|
wrex |
|
74 |
73 9 6
|
wrex |
|
75 |
74 8 6
|
wrex |
|
76 |
75 7 6
|
wrex |
|
77 |
76 5 6
|
wrex |
|
78 |
44 61 77
|
w3o |
|
79 |
78 3 4
|
crab |
|
80 |
1 2 79
|
cmpt |
|
81 |
|
c1 |
|
82 |
36 81
|
cpr |
|
83 |
80 82
|
crdg |
|
84 |
|
com |
|
85 |
83 84
|
cima |
|
86 |
0 85
|
wceq |
|