Step | Hyp | Ref
| Expression |
1 | | simpll 763 |
. . . . 5
β’ (((π΄ β π β§ π΅ β π) β§ (π΅ β π β§ πΆ β π)) β π΄ β π) |
2 | | simplr 765 |
. . . . 5
β’ (((π΄ β π β§ π΅ β π) β§ (π΅ β π β§ πΆ β π)) β π΅ β π) |
3 | | simprr 769 |
. . . . 5
β’ (((π΄ β π β§ π΅ β π) β§ (π΅ β π β§ πΆ β π)) β πΆ β π) |
4 | 1, 2, 3 | 3jca 1126 |
. . . 4
β’ (((π΄ β π β§ π΅ β π) β§ (π΅ β π β§ πΆ β π)) β (π΄ β π β§ π΅ β π β§ πΆ β π)) |
5 | | simplr1 1213 |
. . . . . 6
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β§ ((π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©) β§ (π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©))) β π΄ β π) |
6 | | simplr3 1215 |
. . . . . 6
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β§ ((π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©) β§ (π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©))) β πΆ β π) |
7 | | df-3an 1087 |
. . . . . . . . . . . 12
β’ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΄ Btwn β¨π, π΅β© β§ π΅ Btwn β¨π, πΆβ©) β (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΄ Btwn β¨π, π΅β©) β§ π΅ Btwn β¨π, πΆβ©)) |
8 | | simp1 1134 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β π β β) |
9 | | simp3r 1200 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β π β (πΌβπ)) |
10 | | simp2l 1197 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β π΄ β (πΌβπ)) |
11 | | simp2r 1198 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β π΅ β (πΌβπ)) |
12 | | simp3l 1199 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β πΆ β (πΌβπ)) |
13 | | simpr2 1193 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΄ Btwn β¨π, π΅β© β§ π΅ Btwn β¨π, πΆβ©)) β π΄ Btwn β¨π, π΅β©) |
14 | | simpr3 1194 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΄ Btwn β¨π, π΅β© β§ π΅ Btwn β¨π, πΆβ©)) β π΅ Btwn β¨π, πΆβ©) |
15 | 8, 9, 10, 11, 12, 13, 14 | btwnexchand 35302 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΄ Btwn β¨π, π΅β© β§ π΅ Btwn β¨π, πΆβ©)) β π΄ Btwn β¨π, πΆβ©) |
16 | 15 | orcd 869 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΄ Btwn β¨π, π΅β© β§ π΅ Btwn β¨π, πΆβ©)) β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©)) |
17 | 7, 16 | sylan2br 593 |
. . . . . . . . . . 11
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΄ Btwn β¨π, π΅β©) β§ π΅ Btwn β¨π, πΆβ©)) β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©)) |
18 | 17 | expr 455 |
. . . . . . . . . 10
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΄ Btwn β¨π, π΅β©)) β (π΅ Btwn β¨π, πΆβ© β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©))) |
19 | | simprlr 776 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΄ Btwn β¨π, π΅β©) β§ πΆ Btwn β¨π, π΅β©)) β π΄ Btwn β¨π, π΅β©) |
20 | | simprr 769 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΄ Btwn β¨π, π΅β©) β§ πΆ Btwn β¨π, π΅β©)) β πΆ Btwn β¨π, π΅β©) |
21 | | btwnconn3 35379 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π΅ β (πΌβπ))) β ((π΄ Btwn β¨π, π΅β© β§ πΆ Btwn β¨π, π΅β©) β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©))) |
22 | 8, 9, 10, 12, 11, 21 | syl122anc 1377 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β ((π΄ Btwn β¨π, π΅β© β§ πΆ Btwn β¨π, π΅β©) β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©))) |
23 | 22 | adantr 479 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΄ Btwn β¨π, π΅β©) β§ πΆ Btwn β¨π, π΅β©)) β ((π΄ Btwn β¨π, π΅β© β§ πΆ Btwn β¨π, π΅β©) β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©))) |
24 | 19, 20, 23 | mp2and 695 |
. . . . . . . . . . 11
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΄ Btwn β¨π, π΅β©) β§ πΆ Btwn β¨π, π΅β©)) β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©)) |
25 | 24 | expr 455 |
. . . . . . . . . 10
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΄ Btwn β¨π, π΅β©)) β (πΆ Btwn β¨π, π΅β© β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©))) |
26 | 18, 25 | jaod 855 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΄ Btwn β¨π, π΅β©)) β ((π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©) β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©))) |
27 | 26 | expr 455 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄ Btwn β¨π, π΅β© β ((π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©) β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©)))) |
28 | | simpll2 1211 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π΅ Btwn β¨π, πΆβ©) β π΅ β π) |
29 | 28 | adantl 480 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π΅ Btwn β¨π, πΆβ©)) β π΅ β π) |
30 | 29 | necomd 2994 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π΅ Btwn β¨π, πΆβ©)) β π β π΅) |
31 | | simprlr 776 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π΅ Btwn β¨π, πΆβ©)) β π΅ Btwn β¨π, π΄β©) |
32 | | simprr 769 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π΅ Btwn β¨π, πΆβ©)) β π΅ Btwn β¨π, πΆβ©) |
33 | | btwnconn1 35377 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (π΄ β (πΌβπ) β§ πΆ β (πΌβπ))) β ((π β π΅ β§ π΅ Btwn β¨π, π΄β© β§ π΅ Btwn β¨π, πΆβ©) β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©))) |
34 | 8, 9, 11, 10, 12, 33 | syl122anc 1377 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β ((π β π΅ β§ π΅ Btwn β¨π, π΄β© β§ π΅ Btwn β¨π, πΆβ©) β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©))) |
35 | 34 | adantr 479 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π΅ Btwn β¨π, πΆβ©)) β ((π β π΅ β§ π΅ Btwn β¨π, π΄β© β§ π΅ Btwn β¨π, πΆβ©) β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©))) |
36 | 30, 31, 32, 35 | mp3and 1462 |
. . . . . . . . . . 11
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΅ Btwn β¨π, π΄β©) β§ π΅ Btwn β¨π, πΆβ©)) β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©)) |
37 | 36 | expr 455 |
. . . . . . . . . 10
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΅ Btwn β¨π, π΄β©)) β (π΅ Btwn β¨π, πΆβ© β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©))) |
38 | | df-3an 1087 |
. . . . . . . . . . . 12
β’ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΅ Btwn β¨π, π΄β© β§ πΆ Btwn β¨π, π΅β©) β (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΅ Btwn β¨π, π΄β©) β§ πΆ Btwn β¨π, π΅β©)) |
39 | | simpr3 1194 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΅ Btwn β¨π, π΄β© β§ πΆ Btwn β¨π, π΅β©)) β πΆ Btwn β¨π, π΅β©) |
40 | | simpr2 1193 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΅ Btwn β¨π, π΄β© β§ πΆ Btwn β¨π, π΅β©)) β π΅ Btwn β¨π, π΄β©) |
41 | 8, 9, 12, 11, 10, 39, 40 | btwnexchand 35302 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΅ Btwn β¨π, π΄β© β§ πΆ Btwn β¨π, π΅β©)) β πΆ Btwn β¨π, π΄β©) |
42 | 41 | olcd 870 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΅ Btwn β¨π, π΄β© β§ πΆ Btwn β¨π, π΅β©)) β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©)) |
43 | 38, 42 | sylan2br 593 |
. . . . . . . . . . 11
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΅ Btwn β¨π, π΄β©) β§ πΆ Btwn β¨π, π΅β©)) β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©)) |
44 | 43 | expr 455 |
. . . . . . . . . 10
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΅ Btwn β¨π, π΄β©)) β (πΆ Btwn β¨π, π΅β© β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©))) |
45 | 37, 44 | jaod 855 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ π΅ Btwn β¨π, π΄β©)) β ((π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©) β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©))) |
46 | 45 | expr 455 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΅ Btwn β¨π, π΄β© β ((π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©) β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©)))) |
47 | 27, 46 | jaod 855 |
. . . . . . 7
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©) β ((π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©) β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©)))) |
48 | 47 | imp32 417 |
. . . . . 6
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β§ ((π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©) β§ (π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©))) β (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©)) |
49 | 5, 6, 48 | 3jca 1126 |
. . . . 5
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β§ ((π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©) β§ (π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©))) β (π΄ β π β§ πΆ β π β§ (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©))) |
50 | 49 | exp31 418 |
. . . 4
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β ((π΄ β π β§ π΅ β π β§ πΆ β π) β (((π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©) β§ (π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©)) β (π΄ β π β§ πΆ β π β§ (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©))))) |
51 | 4, 50 | syl5 34 |
. . 3
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β (((π΄ β π β§ π΅ β π) β§ (π΅ β π β§ πΆ β π)) β (((π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©) β§ (π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©)) β (π΄ β π β§ πΆ β π β§ (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©))))) |
52 | 51 | impd 409 |
. 2
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β ((((π΄ β π β§ π΅ β π) β§ (π΅ β π β§ πΆ β π)) β§ ((π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©) β§ (π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©))) β (π΄ β π β§ πΆ β π β§ (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©)))) |
53 | | broutsideof2 35398 |
. . . . 5
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β (π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)))) |
54 | 8, 9, 10, 11, 53 | syl13anc 1370 |
. . . 4
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β (π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)))) |
55 | | broutsideof2 35398 |
. . . . 5
β’ ((π β β β§ (π β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (πOutsideOfβ¨π΅, πΆβ© β (π΅ β π β§ πΆ β π β§ (π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©)))) |
56 | 8, 9, 11, 12, 55 | syl13anc 1370 |
. . . 4
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β (πOutsideOfβ¨π΅, πΆβ© β (π΅ β π β§ πΆ β π β§ (π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©)))) |
57 | 54, 56 | anbi12d 629 |
. . 3
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β ((πOutsideOfβ¨π΄, π΅β© β§ πOutsideOfβ¨π΅, πΆβ©) β ((π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) β§ (π΅ β π β§ πΆ β π β§ (π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©))))) |
58 | | df-3an 1087 |
. . . . 5
β’ ((π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) β ((π΄ β π β§ π΅ β π) β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©))) |
59 | | df-3an 1087 |
. . . . 5
β’ ((π΅ β π β§ πΆ β π β§ (π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©)) β ((π΅ β π β§ πΆ β π) β§ (π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©))) |
60 | 58, 59 | anbi12i 625 |
. . . 4
β’ (((π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) β§ (π΅ β π β§ πΆ β π β§ (π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©))) β (((π΄ β π β§ π΅ β π) β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) β§ ((π΅ β π β§ πΆ β π) β§ (π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©)))) |
61 | | an4 652 |
. . . 4
β’ ((((π΄ β π β§ π΅ β π) β§ (π΅ β π β§ πΆ β π)) β§ ((π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©) β§ (π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©))) β (((π΄ β π β§ π΅ β π) β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) β§ ((π΅ β π β§ πΆ β π) β§ (π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©)))) |
62 | 60, 61 | bitr4i 277 |
. . 3
β’ (((π΄ β π β§ π΅ β π β§ (π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©)) β§ (π΅ β π β§ πΆ β π β§ (π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©))) β (((π΄ β π β§ π΅ β π) β§ (π΅ β π β§ πΆ β π)) β§ ((π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©) β§ (π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©)))) |
63 | 57, 62 | bitrdi 286 |
. 2
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β ((πOutsideOfβ¨π΄, π΅β© β§ πOutsideOfβ¨π΅, πΆβ©) β (((π΄ β π β§ π΅ β π) β§ (π΅ β π β§ πΆ β π)) β§ ((π΄ Btwn β¨π, π΅β© β¨ π΅ Btwn β¨π, π΄β©) β§ (π΅ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΅β©))))) |
64 | | broutsideof2 35398 |
. . 3
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ πΆ β (πΌβπ))) β (πOutsideOfβ¨π΄, πΆβ© β (π΄ β π β§ πΆ β π β§ (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©)))) |
65 | 8, 9, 10, 12, 64 | syl13anc 1370 |
. 2
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β (πOutsideOfβ¨π΄, πΆβ© β (π΄ β π β§ πΆ β π β§ (π΄ Btwn β¨π, πΆβ© β¨ πΆ Btwn β¨π, π΄β©)))) |
66 | 52, 63, 65 | 3imtr4d 293 |
1
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ))) β ((πOutsideOfβ¨π΄, π΅β© β§ πOutsideOfβ¨π΅, πΆβ©) β πOutsideOfβ¨π΄, πΆβ©)) |