Step | Hyp | Ref
| Expression |
1 | | elex 3212 |
. 2
LinesEE |
2 | | ovex 6678 |
. . . . . . 7
Line |
3 | | eleq1 2689 |
. . . . . . 7
Line
Line |
4 | 2, 3 | mpbiri 248 |
. . . . . 6
Line
|
5 | 4 | adantl 482 |
. . . . 5
Line
|
6 | 5 | rexlimivw 3029 |
. . . 4
Line
|
7 | 6 | a1i 11 |
. . 3
Line
|
8 | 7 | rexlimivv 3036 |
. 2
Line
|
9 | | eleq1 2689 |
. . 3
LinesEE
LinesEE |
10 | | eqeq1 2626 |
. . . . . 6
Line
Line |
11 | 10 | anbi2d 740 |
. . . . 5
Line
Line |
12 | 11 | rexbidv 3052 |
. . . 4
Line
Line |
13 | 12 | 2rexbidv 3057 |
. . 3
Line
Line |
14 | | df-lines2 32246 |
. . . . . 6
LinesEE Line |
15 | | df-line2 32244 |
. . . . . . 7
Line
|
16 | 15 | rneqi 5352 |
. . . . . 6
Line
|
17 | | rnoprab 6743 |
. . . . . 6
|
18 | 14, 16, 17 | 3eqtri 2648 |
. . . . 5
LinesEE
|
19 | 18 | eleq2i 2693 |
. . . 4
LinesEE
|
20 | | abid 2610 |
. . . . 5
|
21 | | df-rex 2918 |
. . . . . . 7
|
22 | 21 | 2exbii 1775 |
. . . . . 6
|
23 | | exrot3 2045 |
. . . . . . 7
Line
Line |
24 | | r2ex 3061 |
. . . . . . . 8
Line
Line |
25 | | r19.42v 3092 |
. . . . . . . . . 10
Line
Line |
26 | | df-rex 2918 |
. . . . . . . . . 10
Line
Line |
27 | 25, 26 | bitr3i 266 |
. . . . . . . . 9
Line
Line |
28 | 27 | 2exbii 1775 |
. . . . . . . 8
Line
Line |
29 | 24, 28 | bitri 264 |
. . . . . . 7
Line
Line |
30 | | anass 681 |
. . . . . . . . . 10
Line
Line |
31 | | anass 681 |
. . . . . . . . . . 11
Line
Line |
32 | | simplrl 800 |
. . . . . . . . . . . . . 14
|
33 | | simplrr 801 |
. . . . . . . . . . . . . . 15
|
34 | | simpll 790 |
. . . . . . . . . . . . . . 15
|
35 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
36 | 33, 34, 35 | 3jca 1242 |
. . . . . . . . . . . . . 14
|
37 | 32, 36 | jca 554 |
. . . . . . . . . . . . 13
|
38 | | simpr2 1068 |
. . . . . . . . . . . . . . 15
|
39 | | simpl 473 |
. . . . . . . . . . . . . . 15
|
40 | | simpr1 1067 |
. . . . . . . . . . . . . . 15
|
41 | 38, 39, 40 | jca32 558 |
. . . . . . . . . . . . . 14
|
42 | | simpr3 1069 |
. . . . . . . . . . . . . 14
|
43 | 41, 42 | jca 554 |
. . . . . . . . . . . . 13
|
44 | 37, 43 | impbii 199 |
. . . . . . . . . . . 12
|
45 | 44 | anbi1i 731 |
. . . . . . . . . . 11
Line
Line |
46 | 31, 45 | bitr3i 266 |
. . . . . . . . . 10
Line
Line |
47 | 30, 46 | bitr3i 266 |
. . . . . . . . 9
Line
Line |
48 | | fvline 32251 |
. . . . . . . . . . . 12
Line |
49 | | opex 4932 |
. . . . . . . . . . . . . 14
|
50 | | dfec2 7745 |
. . . . . . . . . . . . . 14
|
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . . . 13
|
52 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
53 | 49, 52 | brcnv 5305 |
. . . . . . . . . . . . . 14
|
54 | 53 | abbii 2739 |
. . . . . . . . . . . . 13
|
55 | 51, 54 | eqtri 2644 |
. . . . . . . . . . . 12
|
56 | 48, 55 | syl6eqr 2674 |
. . . . . . . . . . 11
Line |
57 | 56 | eqeq2d 2632 |
. . . . . . . . . 10
Line
|
58 | 57 | pm5.32i 669 |
. . . . . . . . 9
Line
|
59 | | anass 681 |
. . . . . . . . 9
|
60 | 47, 58, 59 | 3bitrri 287 |
. . . . . . . 8
Line |
61 | 60 | 3exbii 1776 |
. . . . . . 7
Line |
62 | 23, 29, 61 | 3bitr4ri 293 |
. . . . . 6
Line |
63 | 22, 62 | bitri 264 |
. . . . 5
Line |
64 | 20, 63 | bitri 264 |
. . . 4
Line |
65 | 19, 64 | bitri 264 |
. . 3
LinesEE
Line |
66 | 9, 13, 65 | vtoclbg 3267 |
. 2
LinesEE
Line |
67 | 1, 8, 66 | pm5.21nii 368 |
1
LinesEE
Line |