Proof of Theorem dp35lemb
Step | Hyp | Ref
| Expression |
1 | | dp35lem.3 |
. . . . . . 7
c2 a0 a1 b0 b1 |
2 | 1 | ran 78 |
. . . . . 6
c2 c0 c1 a0 a1 b0 b1 c0
c1 |
3 | | an32 83 |
. . . . . 6
a0 a1
b0 b1 c0 c1 a0
a1
c0 c1 b0 b1 |
4 | 2, 3 | tr 62 |
. . . . 5
c2 c0 c1 a0 a1 c0 c1 b0
b1 |
5 | 4 | lor 70 |
. . . 4
b1 c2 c0 c1 b1 a0 a1 c0 c1 b0
b1 |
6 | | leor 159 |
. . . . 5
b1 b0 b1 |
7 | 6 | ml2i 1123 |
. . . 4
b1 a0
a1
c0 c1 b0 b1 b1
a0 a1
c0 c1 b0 b1 |
8 | | ancom 74 |
. . . 4
b1
a0 a1
c0 c1 b0 b1 b0 b1 b1 a0 a1
c0 c1 |
9 | 5, 7, 8 | 3tr 65 |
. . 3
b1 c2 c0 c1 b0 b1 b1 a0 a1
c0 c1 |
10 | 9 | lan 77 |
. 2
b0 b1 c2 c0
c1 b0 b0 b1 b1 a0 a1
c0 c1 |
11 | | anass 76 |
. . 3
b0
b0 b1 b1 a0 a1 c0 c1 b0 b0 b1 b1 a0 a1
c0 c1 |
12 | 11 | cm 61 |
. 2
b0 b0 b1 b1 a0 a1
c0 c1 b0 b0 b1 b1
a0 a1
c0 c1 |
13 | | anabs 121 |
. . 3
b0 b0 b1 b0 |
14 | 13 | ran 78 |
. 2
b0
b0 b1 b1 a0 a1 c0 c1 b0 b1 a0 a1
c0 c1 |
15 | 10, 12, 14 | 3tr 65 |
1
b0 b1 c2 c0
c1 b0 b1 a0 a1
c0 c1 |