Step | Hyp | Ref
| Expression |
1 | | broutsideof2 35771 |
. 2
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β (π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)))) |
2 | | simpl 481 |
. . . . . . . . . 10
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π β β) |
3 | | simpr3 1193 |
. . . . . . . . . 10
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π΅ β (πΌβπ)) |
4 | | simpr1 1191 |
. . . . . . . . . 10
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π β (πΌβπ)) |
5 | | btwndiff 35676 |
. . . . . . . . . 10
β’ ((π β β β§ π΅ β (πΌβπ) β§ π β (πΌβπ)) β βπ β (πΌβπ)(π Btwn β¨π΅, πβ© β§ π β π)) |
6 | 2, 3, 4, 5 | syl3anc 1368 |
. . . . . . . . 9
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β βπ β (πΌβπ)(π Btwn β¨π΅, πβ© β§ π β π)) |
7 | 6 | adantr 479 |
. . . . . . . 8
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©)) β βπ β (πΌβπ)(π Btwn β¨π΅, πβ© β§ π β π)) |
8 | | df-3an 1086 |
. . . . . . . . . . . 12
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ))) |
9 | | 3anass 1092 |
. . . . . . . . . . . 12
β’ ((((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ π Btwn β¨π΅, πβ© β§ π β π) β (((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ (π Btwn β¨π΅, πβ© β§ π β π))) |
10 | | simpr3 1193 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ π Btwn β¨π΅, πβ© β§ π β π)) β π β π) |
11 | 10 | necomd 2986 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ π Btwn β¨π΅, πβ© β§ π β π)) β π β π) |
12 | | simp1 1133 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β π β β) |
13 | | simp23 1205 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β π΅ β (πΌβπ)) |
14 | | simp22 1204 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β π΄ β (πΌβπ)) |
15 | | simp21 1203 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β π β (πΌβπ)) |
16 | | simp3 1135 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β π β (πΌβπ)) |
17 | | simpr1r 1228 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ π Btwn β¨π΅, πβ© β§ π β π)) β π΄ Btwn β¨π, π΅β©) |
18 | 12, 14, 15, 13, 17 | btwncomand 35664 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ π Btwn β¨π΅, πβ© β§ π β π)) β π΄ Btwn β¨π΅, πβ©) |
19 | | simpr2 1192 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ π Btwn β¨π΅, πβ© β§ π β π)) β π Btwn β¨π΅, πβ©) |
20 | 12, 13, 14, 15, 16, 18, 19 | btwnexch3and 35670 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ π Btwn β¨π΅, πβ© β§ π β π)) β π Btwn β¨π΄, πβ©) |
21 | 11, 20, 19 | 3jca 1125 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ π Btwn β¨π΅, πβ© β§ π β π)) β (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)) |
22 | 8, 9, 21 | syl2anbr 597 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ (π Btwn β¨π΅, πβ© β§ π β π))) β (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)) |
23 | 22 | expr 455 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ ((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©)) β ((π Btwn β¨π΅, πβ© β§ π β π) β (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
24 | 23 | an32s 650 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©)) β§ π β (πΌβπ)) β ((π Btwn β¨π΅, πβ© β§ π β π) β (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
25 | 24 | reximdva 3158 |
. . . . . . . 8
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©)) β (βπ β (πΌβπ)(π Btwn β¨π΅, πβ© β§ π β π) β βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
26 | 7, 25 | mpd 15 |
. . . . . . 7
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©)) β βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)) |
27 | 26 | expr 455 |
. . . . . 6
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΄ β π β§ π΅ β π)) β (π΄ Btwn β¨π, π΅β© β βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
28 | | simpr2 1192 |
. . . . . . . . . 10
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π΄ β (πΌβπ)) |
29 | | btwndiff 35676 |
. . . . . . . . . 10
β’ ((π β β β§ π΄ β (πΌβπ) β§ π β (πΌβπ)) β βπ β (πΌβπ)(π Btwn β¨π΄, πβ© β§ π β π)) |
30 | 2, 28, 4, 29 | syl3anc 1368 |
. . . . . . . . 9
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β βπ β (πΌβπ)(π Btwn β¨π΄, πβ© β§ π β π)) |
31 | 30 | adantr 479 |
. . . . . . . 8
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©)) β βπ β (πΌβπ)(π Btwn β¨π΄, πβ© β§ π β π)) |
32 | | 3anass 1092 |
. . . . . . . . . . . 12
β’ ((((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π Btwn β¨π΄, πβ© β§ π β π) β (((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ (π Btwn β¨π΄, πβ© β§ π β π))) |
33 | | simpr3 1193 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π Btwn β¨π΄, πβ© β§ π β π)) β π β π) |
34 | 33 | necomd 2986 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π Btwn β¨π΄, πβ© β§ π β π)) β π β π) |
35 | | simpr2 1192 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π Btwn β¨π΄, πβ© β§ π β π)) β π Btwn β¨π΄, πβ©) |
36 | | simpr1r 1228 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π Btwn β¨π΄, πβ© β§ π β π)) β π΅ Btwn β¨π, π΄β©) |
37 | 12, 13, 15, 14, 36 | btwncomand 35664 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π Btwn β¨π΄, πβ© β§ π β π)) β π΅ Btwn β¨π΄, πβ©) |
38 | 12, 14, 13, 15, 16, 37, 35 | btwnexch3and 35670 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π Btwn β¨π΄, πβ© β§ π β π)) β π Btwn β¨π΅, πβ©) |
39 | 34, 35, 38 | 3jca 1125 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π Btwn β¨π΄, πβ© β§ π β π)) β (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)) |
40 | 8, 32, 39 | syl2anbr 597 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ (π Btwn β¨π΄, πβ© β§ π β π))) β (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)) |
41 | 40 | expr 455 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ ((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©)) β ((π Btwn β¨π΄, πβ© β§ π β π) β (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
42 | 41 | an32s 650 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©)) β§ π β (πΌβπ)) β ((π Btwn β¨π΄, πβ© β§ π β π) β (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
43 | 42 | reximdva 3158 |
. . . . . . . 8
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©)) β (βπ β (πΌβπ)(π Btwn β¨π΄, πβ© β§ π β π) β βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
44 | 31, 43 | mpd 15 |
. . . . . . 7
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©)) β βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)) |
45 | 44 | expr 455 |
. . . . . 6
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΄ β π β§ π΅ β π)) β (π΅ Btwn β¨π, π΄β© β βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
46 | 27, 45 | jaod 857 |
. . . . 5
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΄ β π β§ π΅ β π)) β ((π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©) β βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
47 | | simprr1 1218 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ ((π΄ β π β§ π΅ β π) β§ (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) β π β π) |
48 | | simpll 765 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β π β β) |
49 | | simplr1 1212 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β π β (πΌβπ)) |
50 | | simplr2 1213 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β π΄ β (πΌβπ)) |
51 | | simpr 483 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β π β (πΌβπ)) |
52 | | simprr2 1219 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ ((π΄ β π β§ π΅ β π) β§ (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) β π Btwn β¨π΄, πβ©) |
53 | 48, 49, 50, 51, 52 | btwncomand 35664 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ ((π΄ β π β§ π΅ β π) β§ (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) β π Btwn β¨π, π΄β©) |
54 | | simplr3 1214 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β π΅ β (πΌβπ)) |
55 | | simprr3 1220 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ ((π΄ β π β§ π΅ β π) β§ (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) β π Btwn β¨π΅, πβ©) |
56 | 48, 49, 54, 51, 55 | btwncomand 35664 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ ((π΄ β π β§ π΅ β π) β§ (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) β π Btwn β¨π, π΅β©) |
57 | | btwnconn2 35751 |
. . . . . . . . . . 11
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ)) β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β ((π β π β§ π Btwn β¨π, π΄β© β§ π Btwn β¨π, π΅β©) β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) |
58 | 48, 51, 49, 50, 54, 57 | syl122anc 1376 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β ((π β π β§ π Btwn β¨π, π΄β© β§ π Btwn β¨π, π΅β©) β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) |
59 | 58 | adantr 479 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ ((π΄ β π β§ π΅ β π) β§ (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) β ((π β π β§ π Btwn β¨π, π΄β© β§ π Btwn β¨π, π΅β©) β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) |
60 | 47, 53, 56, 59 | mp3and 1460 |
. . . . . . . 8
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ ((π΄ β π β§ π΅ β π) β§ (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) |
61 | 60 | expr 455 |
. . . . . . 7
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ (π΄ β π β§ π΅ β π)) β ((π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©) β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) |
62 | 61 | an32s 650 |
. . . . . 6
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΄ β π β§ π΅ β π)) β§ π β (πΌβπ)) β ((π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©) β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) |
63 | 62 | rexlimdva 3145 |
. . . . 5
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΄ β π β§ π΅ β π)) β (βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©) β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) |
64 | 46, 63 | impbid 211 |
. . . 4
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΄ β π β§ π΅ β π)) β ((π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©) β βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
65 | 64 | pm5.32da 577 |
. . 3
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (((π΄ β π β§ π΅ β π) β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) β ((π΄ β π β§ π΅ β π) β§ βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)))) |
66 | | df-3an 1086 |
. . 3
β’ ((π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) β ((π΄ β π β§ π΅ β π) β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) |
67 | | df-3an 1086 |
. . 3
β’ ((π΄ β π β§ π΅ β π β§ βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)) β ((π΄ β π β§ π΅ β π) β§ βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
68 | 65, 66, 67 | 3bitr4g 313 |
. 2
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β ((π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) β (π΄ β π β§ π΅ β π β§ βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)))) |
69 | 1, 68 | bitrd 278 |
1
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β (π΄ β π β§ π΅ β π β§ βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)))) |