Step |
Hyp |
Ref |
Expression |
1 |
|
mirval.p |
|
2 |
|
mirval.d |
|
3 |
|
mirval.i |
|
4 |
|
mirval.l |
|
5 |
|
mirval.s |
|
6 |
|
mirval.g |
|
7 |
|
mirln2.m |
|
8 |
|
mirln2.d |
|
9 |
|
mirln2.a |
|
10 |
|
mirln2.1 |
|
11 |
|
mirln2.2 |
|
12 |
1 4 3 6 8 10
|
tglnpt |
|
13 |
1 2 3 4 5 6 9 7 12
|
mirinv |
|
14 |
13
|
biimpa |
|
15 |
10
|
adantr |
|
16 |
14 15
|
eqeltrd |
|
17 |
6
|
adantr |
|
18 |
1 4 3 6 8 11
|
tglnpt |
|
19 |
18
|
adantr |
|
20 |
12
|
adantr |
|
21 |
9
|
adantr |
|
22 |
|
simpr |
|
23 |
1 2 3 4 5 17 21 7 20
|
mirbtwn |
|
24 |
1 3 4 17 19 20 21 22 23
|
btwnlng1 |
|
25 |
8
|
adantr |
|
26 |
11
|
adantr |
|
27 |
10
|
adantr |
|
28 |
1 3 4 17 19 20 22 22 25 26 27
|
tglinethru |
|
29 |
24 28
|
eleqtrrd |
|
30 |
16 29
|
pm2.61dane |
|