Step | Hyp | Ref
| Expression |
1 | | broutsideof 35081 |
. 2
β’ (πOutsideOfβ¨π΄, π΅β© β (π Colinear β¨π΄, π΅β© β§ Β¬ π Btwn β¨π΄, π΅β©)) |
2 | | btwntriv1 34976 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β π΄ Btwn β¨π΄, π΅β©) |
3 | 2 | 3adant3r1 1182 |
. . . . . . . 8
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π΄ Btwn β¨π΄, π΅β©) |
4 | | breq1 5150 |
. . . . . . . 8
β’ (π΄ = π β (π΄ Btwn β¨π΄, π΅β© β π Btwn β¨π΄, π΅β©)) |
5 | 3, 4 | syl5ibcom 244 |
. . . . . . 7
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (π΄ = π β π Btwn β¨π΄, π΅β©)) |
6 | 5 | necon3bd 2954 |
. . . . . 6
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (Β¬ π Btwn β¨π΄, π΅β© β π΄ β π)) |
7 | 6 | imp 407 |
. . . . 5
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ Β¬ π Btwn β¨π΄, π΅β©) β π΄ β π) |
8 | 7 | adantrl 714 |
. . . 4
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π Colinear β¨π΄, π΅β© β§ Β¬ π Btwn β¨π΄, π΅β©)) β π΄ β π) |
9 | | btwntriv2 34972 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β π΅ Btwn β¨π΄, π΅β©) |
10 | 9 | 3adant3r1 1182 |
. . . . . . . 8
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π΅ Btwn β¨π΄, π΅β©) |
11 | | breq1 5150 |
. . . . . . . 8
β’ (π΅ = π β (π΅ Btwn β¨π΄, π΅β© β π Btwn β¨π΄, π΅β©)) |
12 | 10, 11 | syl5ibcom 244 |
. . . . . . 7
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (π΅ = π β π Btwn β¨π΄, π΅β©)) |
13 | 12 | necon3bd 2954 |
. . . . . 6
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (Β¬ π Btwn β¨π΄, π΅β© β π΅ β π)) |
14 | 13 | imp 407 |
. . . . 5
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ Β¬ π Btwn β¨π΄, π΅β©) β π΅ β π) |
15 | 14 | adantrl 714 |
. . . 4
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π Colinear β¨π΄, π΅β© β§ Β¬ π Btwn β¨π΄, π΅β©)) β π΅ β π) |
16 | | brcolinear 35019 |
. . . . . 6
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (π Colinear β¨π΄, π΅β© β (π Btwn β¨π΄, π΅β© β¨ π΄ Btwn β¨π΅, πβ© β¨ π΅ Btwn β¨π, π΄β©))) |
17 | | pm2.24 124 |
. . . . . . . 8
β’ (π Btwn β¨π΄, π΅β© β (Β¬ π Btwn β¨π΄, π΅β© β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) |
18 | 17 | a1i 11 |
. . . . . . 7
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (π Btwn β¨π΄, π΅β© β (Β¬ π Btwn β¨π΄, π΅β© β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)))) |
19 | | 3anrot 1100 |
. . . . . . . . . 10
β’ ((π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π β (πΌβπ))) |
20 | | btwncom 34974 |
. . . . . . . . . 10
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π β (πΌβπ))) β (π΄ Btwn β¨π΅, πβ© β π΄ Btwn β¨π, π΅β©)) |
21 | 19, 20 | sylan2b 594 |
. . . . . . . . 9
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (π΄ Btwn β¨π΅, πβ© β π΄ Btwn β¨π, π΅β©)) |
22 | | orc 865 |
. . . . . . . . 9
β’ (π΄ Btwn β¨π, π΅β© β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) |
23 | 21, 22 | syl6bi 252 |
. . . . . . . 8
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (π΄ Btwn β¨π΅, πβ© β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) |
24 | 23 | a1dd 50 |
. . . . . . 7
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (π΄ Btwn β¨π΅, πβ© β (Β¬ π Btwn β¨π΄, π΅β© β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)))) |
25 | | olc 866 |
. . . . . . . . 9
β’ (π΅ Btwn β¨π, π΄β© β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) |
26 | 25 | a1d 25 |
. . . . . . . 8
β’ (π΅ Btwn β¨π, π΄β© β (Β¬ π Btwn β¨π΄, π΅β© β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) |
27 | 26 | a1i 11 |
. . . . . . 7
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (π΅ Btwn β¨π, π΄β© β (Β¬ π Btwn β¨π΄, π΅β© β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)))) |
28 | 18, 24, 27 | 3jaod 1428 |
. . . . . 6
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β ((π Btwn β¨π΄, π΅β© β¨ π΄ Btwn β¨π΅, πβ© β¨ π΅ Btwn β¨π, π΄β©) β (Β¬ π Btwn β¨π΄, π΅β© β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)))) |
29 | 16, 28 | sylbid 239 |
. . . . 5
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (π Colinear β¨π΄, π΅β© β (Β¬ π Btwn β¨π΄, π΅β© β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)))) |
30 | 29 | imp32 419 |
. . . 4
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π Colinear β¨π΄, π΅β© β§ Β¬ π Btwn β¨π΄, π΅β©)) β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) |
31 | 8, 15, 30 | 3jca 1128 |
. . 3
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π Colinear β¨π΄, π΅β© β§ Β¬ π Btwn β¨π΄, π΅β©)) β (π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) |
32 | | simp3 1138 |
. . . . . 6
β’ ((π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) |
33 | | 3ancomb 1099 |
. . . . . . . 8
β’ ((π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β (π β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β (πΌβπ))) |
34 | | btwncolinear2 35030 |
. . . . . . . 8
β’ ((π β β β§ (π β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β (πΌβπ))) β (π΄ Btwn β¨π, π΅β© β π Colinear β¨π΄, π΅β©)) |
35 | 33, 34 | sylan2b 594 |
. . . . . . 7
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (π΄ Btwn β¨π, π΅β© β π Colinear β¨π΄, π΅β©)) |
36 | | btwncolinear1 35029 |
. . . . . . 7
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (π΅ Btwn β¨π, π΄β© β π Colinear β¨π΄, π΅β©)) |
37 | 35, 36 | jaod 857 |
. . . . . 6
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β ((π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©) β π Colinear β¨π΄, π΅β©)) |
38 | 32, 37 | syl5 34 |
. . . . 5
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β ((π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) β π Colinear β¨π΄, π΅β©)) |
39 | 38 | imp 407 |
. . . 4
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) β π Colinear β¨π΄, π΅β©) |
40 | | simpr2 1195 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΄ Btwn β¨π, π΅β© β§ π΄ β π β§ π΅ β π)) β π΄ β π) |
41 | 40 | neneqd 2945 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΄ Btwn β¨π, π΅β© β§ π΄ β π β§ π΅ β π)) β Β¬ π΄ = π) |
42 | | simprl1 1218 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ Btwn β¨π, π΅β© β§ π΄ β π β§ π΅ β π) β§ π Btwn β¨π΄, π΅β©)) β π΄ Btwn β¨π, π΅β©) |
43 | | simprr 771 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ Btwn β¨π, π΅β© β§ π΄ β π β§ π΅ β π) β§ π Btwn β¨π΄, π΅β©)) β π Btwn β¨π΄, π΅β©) |
44 | | simpl 483 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π β β) |
45 | | simpr2 1195 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π΄ β (πΌβπ)) |
46 | | simpr1 1194 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π β (πΌβπ)) |
47 | | simpr3 1196 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π΅ β (πΌβπ)) |
48 | | btwnswapid 34977 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π β (πΌβπ) β§ π΅ β (πΌβπ))) β ((π΄ Btwn β¨π, π΅β© β§ π Btwn β¨π΄, π΅β©) β π΄ = π)) |
49 | 44, 45, 46, 47, 48 | syl13anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β ((π΄ Btwn β¨π, π΅β© β§ π Btwn β¨π΄, π΅β©) β π΄ = π)) |
50 | 49 | adantr 481 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ Btwn β¨π, π΅β© β§ π΄ β π β§ π΅ β π) β§ π Btwn β¨π΄, π΅β©)) β ((π΄ Btwn β¨π, π΅β© β§ π Btwn β¨π΄, π΅β©) β π΄ = π)) |
51 | 42, 43, 50 | mp2and 697 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ Btwn β¨π, π΅β© β§ π΄ β π β§ π΅ β π) β§ π Btwn β¨π΄, π΅β©)) β π΄ = π) |
52 | 51 | expr 457 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΄ Btwn β¨π, π΅β© β§ π΄ β π β§ π΅ β π)) β (π Btwn β¨π΄, π΅β© β π΄ = π)) |
53 | 41, 52 | mtod 197 |
. . . . . . . . 9
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΄ Btwn β¨π, π΅β© β§ π΄ β π β§ π΅ β π)) β Β¬ π Btwn β¨π΄, π΅β©) |
54 | 53 | 3exp2 1354 |
. . . . . . . 8
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (π΄ Btwn β¨π, π΅β© β (π΄ β π β (π΅ β π β Β¬ π Btwn β¨π΄, π΅β©)))) |
55 | | simpr3 1196 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΅ Btwn β¨π, π΄β© β§ π΄ β π β§ π΅ β π)) β π΅ β π) |
56 | 55 | neneqd 2945 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΅ Btwn β¨π, π΄β© β§ π΄ β π β§ π΅ β π)) β Β¬ π΅ = π) |
57 | | simprl1 1218 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΅ Btwn β¨π, π΄β© β§ π΄ β π β§ π΅ β π) β§ π Btwn β¨π΄, π΅β©)) β π΅ Btwn β¨π, π΄β©) |
58 | | simprr 771 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΅ Btwn β¨π, π΄β© β§ π΄ β π β§ π΅ β π) β§ π Btwn β¨π΄, π΅β©)) β π Btwn β¨π΄, π΅β©) |
59 | 44, 46, 45, 47, 58 | btwncomand 34975 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΅ Btwn β¨π, π΄β© β§ π΄ β π β§ π΅ β π) β§ π Btwn β¨π΄, π΅β©)) β π Btwn β¨π΅, π΄β©) |
60 | | 3anrot 1100 |
. . . . . . . . . . . . . 14
β’ ((π΅ β (πΌβπ) β§ π β (πΌβπ) β§ π΄ β (πΌβπ)) β (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) |
61 | | btwnswapid 34977 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π΅ β (πΌβπ) β§ π β (πΌβπ) β§ π΄ β (πΌβπ))) β ((π΅ Btwn β¨π, π΄β© β§ π Btwn β¨π΅, π΄β©) β π΅ = π)) |
62 | 60, 61 | sylan2br 595 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β ((π΅ Btwn β¨π, π΄β© β§ π Btwn β¨π΅, π΄β©) β π΅ = π)) |
63 | 62 | adantr 481 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΅ Btwn β¨π, π΄β© β§ π΄ β π β§ π΅ β π) β§ π Btwn β¨π΄, π΅β©)) β ((π΅ Btwn β¨π, π΄β© β§ π Btwn β¨π΅, π΄β©) β π΅ = π)) |
64 | 57, 59, 63 | mp2and 697 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΅ Btwn β¨π, π΄β© β§ π΄ β π β§ π΅ β π) β§ π Btwn β¨π΄, π΅β©)) β π΅ = π) |
65 | 64 | expr 457 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΅ Btwn β¨π, π΄β© β§ π΄ β π β§ π΅ β π)) β (π Btwn β¨π΄, π΅β© β π΅ = π)) |
66 | 56, 65 | mtod 197 |
. . . . . . . . 9
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΅ Btwn β¨π, π΄β© β§ π΄ β π β§ π΅ β π)) β Β¬ π Btwn β¨π΄, π΅β©) |
67 | 66 | 3exp2 1354 |
. . . . . . . 8
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (π΅ Btwn β¨π, π΄β© β (π΄ β π β (π΅ β π β Β¬ π Btwn β¨π΄, π΅β©)))) |
68 | 54, 67 | jaod 857 |
. . . . . . 7
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β ((π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©) β (π΄ β π β (π΅ β π β Β¬ π Btwn β¨π΄, π΅β©)))) |
69 | 68 | com12 32 |
. . . . . 6
β’ ((π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©) β ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (π΄ β π β (π΅ β π β Β¬ π Btwn β¨π΄, π΅β©)))) |
70 | 69 | com4l 92 |
. . . . 5
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (π΄ β π β (π΅ β π β ((π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©) β Β¬ π Btwn β¨π΄, π΅β©)))) |
71 | 70 | 3imp2 1349 |
. . . 4
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) β Β¬ π Btwn β¨π΄, π΅β©) |
72 | 39, 71 | jca 512 |
. . 3
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) β (π Colinear β¨π΄, π΅β© β§ Β¬ π Btwn β¨π΄, π΅β©)) |
73 | 31, 72 | impbida 799 |
. 2
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β ((π Colinear β¨π΄, π΅β© β§ Β¬ π Btwn β¨π΄, π΅β©) β (π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)))) |
74 | 1, 73 | bitrid 282 |
1
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β (π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)))) |