Step | Hyp | Ref
| Expression |
1 | | broutsideof2 35641 |
. 2
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β (π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)))) |
2 | | simpl 482 |
. . . . . . . . . 10
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π β β) |
3 | | simpr3 1194 |
. . . . . . . . . 10
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π΅ β (πΌβπ)) |
4 | | simpr1 1192 |
. . . . . . . . . 10
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π β (πΌβπ)) |
5 | | btwndiff 35546 |
. . . . . . . . . 10
β’ ((π β β β§ π΅ β (πΌβπ) β§ π β (πΌβπ)) β βπ β (πΌβπ)(π Btwn β¨π΅, πβ© β§ π β π)) |
6 | 2, 3, 4, 5 | syl3anc 1369 |
. . . . . . . . 9
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β βπ β (πΌβπ)(π Btwn β¨π΅, πβ© β§ π β π)) |
7 | 6 | adantr 480 |
. . . . . . . 8
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©)) β βπ β (πΌβπ)(π Btwn β¨π΅, πβ© β§ π β π)) |
8 | | df-3an 1087 |
. . . . . . . . . . . 12
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ))) |
9 | | 3anass 1093 |
. . . . . . . . . . . 12
β’ ((((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ π Btwn β¨π΅, πβ© β§ π β π) β (((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ (π Btwn β¨π΅, πβ© β§ π β π))) |
10 | | simpr3 1194 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ π Btwn β¨π΅, πβ© β§ π β π)) β π β π) |
11 | 10 | necomd 2991 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ π Btwn β¨π΅, πβ© β§ π β π)) β π β π) |
12 | | simp1 1134 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β π β β) |
13 | | simp23 1206 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β π΅ β (πΌβπ)) |
14 | | simp22 1205 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β π΄ β (πΌβπ)) |
15 | | simp21 1204 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β π β (πΌβπ)) |
16 | | simp3 1136 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β π β (πΌβπ)) |
17 | | simpr1r 1229 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ π Btwn β¨π΅, πβ© β§ π β π)) β π΄ Btwn β¨π, π΅β©) |
18 | 12, 14, 15, 13, 17 | btwncomand 35534 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ π Btwn β¨π΅, πβ© β§ π β π)) β π΄ Btwn β¨π΅, πβ©) |
19 | | simpr2 1193 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ π Btwn β¨π΅, πβ© β§ π β π)) β π Btwn β¨π΅, πβ©) |
20 | 12, 13, 14, 15, 16, 18, 19 | btwnexch3and 35540 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ π Btwn β¨π΅, πβ© β§ π β π)) β π Btwn β¨π΄, πβ©) |
21 | 11, 20, 19 | 3jca 1126 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ π Btwn β¨π΅, πβ© β§ π β π)) β (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)) |
22 | 8, 9, 21 | syl2anbr 598 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©) β§ (π Btwn β¨π΅, πβ© β§ π β π))) β (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)) |
23 | 22 | expr 456 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ ((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©)) β ((π Btwn β¨π΅, πβ© β§ π β π) β (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
24 | 23 | an32s 651 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©)) β§ π β (πΌβπ)) β ((π Btwn β¨π΅, πβ© β§ π β π) β (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
25 | 24 | reximdva 3163 |
. . . . . . . 8
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©)) β (βπ β (πΌβπ)(π Btwn β¨π΅, πβ© β§ π β π) β βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
26 | 7, 25 | mpd 15 |
. . . . . . 7
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π) β§ π΄ Btwn β¨π, π΅β©)) β βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)) |
27 | 26 | expr 456 |
. . . . . 6
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΄ β π β§ π΅ β π)) β (π΄ Btwn β¨π, π΅β© β βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
28 | | simpr2 1193 |
. . . . . . . . . 10
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π΄ β (πΌβπ)) |
29 | | btwndiff 35546 |
. . . . . . . . . 10
β’ ((π β β β§ π΄ β (πΌβπ) β§ π β (πΌβπ)) β βπ β (πΌβπ)(π Btwn β¨π΄, πβ© β§ π β π)) |
30 | 2, 28, 4, 29 | syl3anc 1369 |
. . . . . . . . 9
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β βπ β (πΌβπ)(π Btwn β¨π΄, πβ© β§ π β π)) |
31 | 30 | adantr 480 |
. . . . . . . 8
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©)) β βπ β (πΌβπ)(π Btwn β¨π΄, πβ© β§ π β π)) |
32 | | 3anass 1093 |
. . . . . . . . . . . 12
β’ ((((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π Btwn β¨π΄, πβ© β§ π β π) β (((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ (π Btwn β¨π΄, πβ© β§ π β π))) |
33 | | simpr3 1194 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π Btwn β¨π΄, πβ© β§ π β π)) β π β π) |
34 | 33 | necomd 2991 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π Btwn β¨π΄, πβ© β§ π β π)) β π β π) |
35 | | simpr2 1193 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π Btwn β¨π΄, πβ© β§ π β π)) β π Btwn β¨π΄, πβ©) |
36 | | simpr1r 1229 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π Btwn β¨π΄, πβ© β§ π β π)) β π΅ Btwn β¨π, π΄β©) |
37 | 12, 13, 15, 14, 36 | btwncomand 35534 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π Btwn β¨π΄, πβ© β§ π β π)) β π΅ Btwn β¨π΄, πβ©) |
38 | 12, 14, 13, 15, 16, 37, 35 | btwnexch3and 35540 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π Btwn β¨π΄, πβ© β§ π β π)) β π Btwn β¨π΅, πβ©) |
39 | 34, 35, 38 | 3jca 1126 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π Btwn β¨π΄, πβ© β§ π β π)) β (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)) |
40 | 8, 32, 39 | syl2anbr 598 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ (((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©) β§ (π Btwn β¨π΄, πβ© β§ π β π))) β (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)) |
41 | 40 | expr 456 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ ((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©)) β ((π Btwn β¨π΄, πβ© β§ π β π) β (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
42 | 41 | an32s 651 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©)) β§ π β (πΌβπ)) β ((π Btwn β¨π΄, πβ© β§ π β π) β (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
43 | 42 | reximdva 3163 |
. . . . . . . 8
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©)) β (βπ β (πΌβπ)(π Btwn β¨π΄, πβ© β§ π β π) β βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
44 | 31, 43 | mpd 15 |
. . . . . . 7
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π) β§ π΅ Btwn β¨π, π΄β©)) β βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)) |
45 | 44 | expr 456 |
. . . . . 6
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΄ β π β§ π΅ β π)) β (π΅ Btwn β¨π, π΄β© β βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
46 | 27, 45 | jaod 858 |
. . . . 5
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΄ β π β§ π΅ β π)) β ((π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©) β βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
47 | | simprr1 1219 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ ((π΄ β π β§ π΅ β π) β§ (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) β π β π) |
48 | | simpll 766 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β π β β) |
49 | | simplr1 1213 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β π β (πΌβπ)) |
50 | | simplr2 1214 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β π΄ β (πΌβπ)) |
51 | | simpr 484 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β π β (πΌβπ)) |
52 | | simprr2 1220 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ ((π΄ β π β§ π΅ β π) β§ (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) β π Btwn β¨π΄, πβ©) |
53 | 48, 49, 50, 51, 52 | btwncomand 35534 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ ((π΄ β π β§ π΅ β π) β§ (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) β π Btwn β¨π, π΄β©) |
54 | | simplr3 1215 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β π΅ β (πΌβπ)) |
55 | | simprr3 1221 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ ((π΄ β π β§ π΅ β π) β§ (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) β π Btwn β¨π΅, πβ©) |
56 | 48, 49, 54, 51, 55 | btwncomand 35534 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ ((π΄ β π β§ π΅ β π) β§ (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) β π Btwn β¨π, π΅β©) |
57 | | btwnconn2 35621 |
. . . . . . . . . . 11
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ)) β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β ((π β π β§ π Btwn β¨π, π΄β© β§ π Btwn β¨π, π΅β©) β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) |
58 | 48, 51, 49, 50, 54, 57 | syl122anc 1377 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β ((π β π β§ π Btwn β¨π, π΄β© β§ π Btwn β¨π, π΅β©) β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) |
59 | 58 | adantr 480 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ ((π΄ β π β§ π΅ β π) β§ (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) β ((π β π β§ π Btwn β¨π, π΄β© β§ π Btwn β¨π, π΅β©) β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) |
60 | 47, 53, 56, 59 | mp3and 1461 |
. . . . . . . 8
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ ((π΄ β π β§ π΅ β π) β§ (π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) |
61 | 60 | expr 456 |
. . . . . . 7
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π β (πΌβπ)) β§ (π΄ β π β§ π΅ β π)) β ((π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©) β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) |
62 | 61 | an32s 651 |
. . . . . 6
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΄ β π β§ π΅ β π)) β§ π β (πΌβπ)) β ((π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©) β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) |
63 | 62 | rexlimdva 3150 |
. . . . 5
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΄ β π β§ π΅ β π)) β (βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©) β (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) |
64 | 46, 63 | impbid 211 |
. . . 4
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ (π΄ β π β§ π΅ β π)) β ((π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©) β βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
65 | 64 | pm5.32da 578 |
. . 3
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (((π΄ β π β§ π΅ β π) β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) β ((π΄ β π β§ π΅ β π) β§ βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)))) |
66 | | df-3an 1087 |
. . 3
β’ ((π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) β ((π΄ β π β§ π΅ β π) β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) |
67 | | df-3an 1087 |
. . 3
β’ ((π΄ β π β§ π΅ β π β§ βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)) β ((π΄ β π β§ π΅ β π) β§ βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©))) |
68 | 65, 66, 67 | 3bitr4g 314 |
. 2
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β ((π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) β (π΄ β π β§ π΅ β π β§ βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)))) |
69 | 1, 68 | bitrd 279 |
1
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β (π΄ β π β§ π΅ β π β§ βπ β (πΌβπ)(π β π β§ π Btwn β¨π΄, πβ© β§ π Btwn β¨π΅, πβ©)))) |