Step | Hyp | Ref
| Expression |
1 | | simprll 778 |
. . . . . . 7
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ))) β§ ((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©))) β π¦ Btwn β¨πΆ, π·β©) |
2 | | simprrr 781 |
. . . . . . 7
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ))) β§ ((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©))) β β¨πΆ, π·β©Cgrβ¨πΈ, π§β©) |
3 | 1, 2 | jca 513 |
. . . . . 6
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ))) β§ ((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©))) β (π¦ Btwn β¨πΆ, π·β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©)) |
4 | | simpl1 1192 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ))) β π β β) |
5 | | simpl23 1254 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ))) β πΆ β (πΌβπ)) |
6 | | simprl 770 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ))) β π¦ β (πΌβπ)) |
7 | | simpl31 1255 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ))) β π· β (πΌβπ)) |
8 | | simpl32 1256 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ))) β πΈ β (πΌβπ)) |
9 | | simprr 772 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ))) β π§ β (πΌβπ)) |
10 | | cgrxfr 34686 |
. . . . . . . 8
β’ ((π β β β§ (πΆ β (πΌβπ) β§ π¦ β (πΌβπ) β§ π· β (πΌβπ)) β§ (πΈ β (πΌβπ) β§ π§ β (πΌβπ))) β ((π¦ Btwn β¨πΆ, π·β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©) β βπ€ β (πΌβπ)(π€ Btwn β¨πΈ, π§β© β§ β¨πΆ, β¨π¦, π·β©β©Cgr3β¨πΈ, β¨π€, π§β©β©))) |
11 | 4, 5, 6, 7, 8, 9, 10 | syl132anc 1389 |
. . . . . . 7
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ))) β ((π¦ Btwn β¨πΆ, π·β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©) β βπ€ β (πΌβπ)(π€ Btwn β¨πΈ, π§β© β§ β¨πΆ, β¨π¦, π·β©β©Cgr3β¨πΈ, β¨π€, π§β©β©))) |
12 | 11 | adantr 482 |
. . . . . 6
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ))) β§ ((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©))) β ((π¦ Btwn β¨πΆ, π·β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©) β βπ€ β (πΌβπ)(π€ Btwn β¨πΈ, π§β© β§ β¨πΆ, β¨π¦, π·β©β©Cgr3β¨πΈ, β¨π€, π§β©β©))) |
13 | 3, 12 | mpd 15 |
. . . . 5
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ))) β§ ((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©))) β βπ€ β (πΌβπ)(π€ Btwn β¨πΈ, π§β© β§ β¨πΆ, β¨π¦, π·β©β©Cgr3β¨πΈ, β¨π€, π§β©β©)) |
14 | | anass 470 |
. . . . . . . . 9
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ))) β§ π€ β (πΌβπ)) β ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ ((π¦ β (πΌβπ) β§ π§ β (πΌβπ)) β§ π€ β (πΌβπ)))) |
15 | | df-3an 1090 |
. . . . . . . . . 10
β’ ((π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ)) β ((π¦ β (πΌβπ) β§ π§ β (πΌβπ)) β§ π€ β (πΌβπ))) |
16 | 15 | anbi2i 624 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ ((π¦ β (πΌβπ) β§ π§ β (πΌβπ)) β§ π€ β (πΌβπ)))) |
17 | 14, 16 | bitr4i 278 |
. . . . . . . 8
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ))) β§ π€ β (πΌβπ)) β ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ)))) |
18 | | simpl1 1192 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β π β β) |
19 | | simpl23 1254 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β πΆ β (πΌβπ)) |
20 | | simpr1 1195 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β π¦ β (πΌβπ)) |
21 | | simpl31 1255 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β π· β (πΌβπ)) |
22 | | simpl32 1256 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β πΈ β (πΌβπ)) |
23 | | simpr3 1197 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β π€ β (πΌβπ)) |
24 | | simpr2 1196 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β π§ β (πΌβπ)) |
25 | | brcgr3 34677 |
. . . . . . . . . . . 12
β’ ((π β β β§ (πΆ β (πΌβπ) β§ π¦ β (πΌβπ) β§ π· β (πΌβπ)) β§ (πΈ β (πΌβπ) β§ π€ β (πΌβπ) β§ π§ β (πΌβπ))) β (β¨πΆ, β¨π¦, π·β©β©Cgr3β¨πΈ, β¨π€, π§β©β© β (β¨πΆ, π¦β©Cgrβ¨πΈ, π€β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β© β§ β¨π¦, π·β©Cgrβ¨π€, π§β©))) |
26 | 18, 19, 20, 21, 22, 23, 24, 25 | syl133anc 1394 |
. . . . . . . . . . 11
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β (β¨πΆ, β¨π¦, π·β©β©Cgr3β¨πΈ, β¨π€, π§β©β© β (β¨πΆ, π¦β©Cgrβ¨πΈ, π€β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β© β§ β¨π¦, π·β©Cgrβ¨π€, π§β©))) |
27 | 26 | anbi2d 630 |
. . . . . . . . . 10
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β ((π€ Btwn β¨πΈ, π§β© β§ β¨πΆ, β¨π¦, π·β©β©Cgr3β¨πΈ, β¨π€, π§β©β©) β (π€ Btwn β¨πΈ, π§β© β§ (β¨πΆ, π¦β©Cgrβ¨πΈ, π€β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β© β§ β¨π¦, π·β©Cgrβ¨π€, π§β©)))) |
28 | 27 | adantr 482 |
. . . . . . . . 9
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β§ ((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©))) β ((π€ Btwn β¨πΈ, π§β© β§ β¨πΆ, β¨π¦, π·β©β©Cgr3β¨πΈ, β¨π€, π§β©β©) β (π€ Btwn β¨πΈ, π§β© β§ (β¨πΆ, π¦β©Cgrβ¨πΈ, π€β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β© β§ β¨π¦, π·β©Cgrβ¨π€, π§β©)))) |
29 | | df-3an 1090 |
. . . . . . . . . . 11
β’ (((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©) β§ (π€ Btwn β¨πΈ, π§β© β§ (β¨πΆ, π¦β©Cgrβ¨πΈ, π€β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β© β§ β¨π¦, π·β©Cgrβ¨π€, π§β©))) β (((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©)) β§ (π€ Btwn β¨πΈ, π§β© β§ (β¨πΆ, π¦β©Cgrβ¨πΈ, π€β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β© β§ β¨π¦, π·β©Cgrβ¨π€, π§β©)))) |
30 | | simpl33 1257 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β πΉ β (πΌβπ)) |
31 | | simpr3l 1235 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β§ ((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©) β§ (π€ Btwn β¨πΈ, π§β© β§ (β¨πΆ, π¦β©Cgrβ¨πΈ, π€β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β© β§ β¨π¦, π·β©Cgrβ¨π€, π§β©)))) β π€ Btwn β¨πΈ, π§β©) |
32 | | simpr2l 1233 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β§ ((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©) β§ (π€ Btwn β¨πΈ, π§β© β§ (β¨πΆ, π¦β©Cgrβ¨πΈ, π€β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β© β§ β¨π¦, π·β©Cgrβ¨π€, π§β©)))) β π§ Btwn β¨πΈ, πΉβ©) |
33 | 18, 22, 23, 24, 30, 31, 32 | btwnexchand 34657 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β§ ((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©) β§ (π€ Btwn β¨πΈ, π§β© β§ (β¨πΆ, π¦β©Cgrβ¨πΈ, π€β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β© β§ β¨π¦, π·β©Cgrβ¨π€, π§β©)))) β π€ Btwn β¨πΈ, πΉβ©) |
34 | | simpl21 1252 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β π΄ β (πΌβπ)) |
35 | | simpl22 1253 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β π΅ β (πΌβπ)) |
36 | | simpr1r 1232 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β§ ((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©) β§ (π€ Btwn β¨πΈ, π§β© β§ (β¨πΆ, π¦β©Cgrβ¨πΈ, π€β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β© β§ β¨π¦, π·β©Cgrβ¨π€, π§β©)))) β β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) |
37 | | simp3r1 1282 |
. . . . . . . . . . . . . 14
β’ (((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©) β§ (π€ Btwn β¨πΈ, π§β© β§ (β¨πΆ, π¦β©Cgrβ¨πΈ, π€β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β© β§ β¨π¦, π·β©Cgrβ¨π€, π§β©))) β β¨πΆ, π¦β©Cgrβ¨πΈ, π€β©) |
38 | 37 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β§ ((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©) β§ (π€ Btwn β¨πΈ, π§β© β§ (β¨πΆ, π¦β©Cgrβ¨πΈ, π€β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β© β§ β¨π¦, π·β©Cgrβ¨π€, π§β©)))) β β¨πΆ, π¦β©Cgrβ¨πΈ, π€β©) |
39 | 18, 34, 35, 19, 20, 22, 23, 36, 38 | cgrtrand 34624 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β§ ((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©) β§ (π€ Btwn β¨πΈ, π§β© β§ (β¨πΆ, π¦β©Cgrβ¨πΈ, π€β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β© β§ β¨π¦, π·β©Cgrβ¨π€, π§β©)))) β β¨π΄, π΅β©Cgrβ¨πΈ, π€β©) |
40 | 33, 39 | jca 513 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β§ ((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©) β§ (π€ Btwn β¨πΈ, π§β© β§ (β¨πΆ, π¦β©Cgrβ¨πΈ, π€β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β© β§ β¨π¦, π·β©Cgrβ¨π€, π§β©)))) β (π€ Btwn β¨πΈ, πΉβ© β§ β¨π΄, π΅β©Cgrβ¨πΈ, π€β©)) |
41 | 29, 40 | sylan2br 596 |
. . . . . . . . . 10
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β§ (((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©)) β§ (π€ Btwn β¨πΈ, π§β© β§ (β¨πΆ, π¦β©Cgrβ¨πΈ, π€β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β© β§ β¨π¦, π·β©Cgrβ¨π€, π§β©)))) β (π€ Btwn β¨πΈ, πΉβ© β§ β¨π΄, π΅β©Cgrβ¨πΈ, π€β©)) |
42 | 41 | expr 458 |
. . . . . . . . 9
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β§ ((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©))) β ((π€ Btwn β¨πΈ, π§β© β§ (β¨πΆ, π¦β©Cgrβ¨πΈ, π€β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β© β§ β¨π¦, π·β©Cgrβ¨π€, π§β©)) β (π€ Btwn β¨πΈ, πΉβ© β§ β¨π΄, π΅β©Cgrβ¨πΈ, π€β©))) |
43 | 28, 42 | sylbid 239 |
. . . . . . . 8
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ) β§ π€ β (πΌβπ))) β§ ((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©))) β ((π€ Btwn β¨πΈ, π§β© β§ β¨πΆ, β¨π¦, π·β©β©Cgr3β¨πΈ, β¨π€, π§β©β©) β (π€ Btwn β¨πΈ, πΉβ© β§ β¨π΄, π΅β©Cgrβ¨πΈ, π€β©))) |
44 | 17, 43 | sylanb 582 |
. . . . . . 7
β’
(((((π β
β β§ (π΄ β
(πΌβπ) β§
π΅ β
(πΌβπ) β§
πΆ β
(πΌβπ)) β§
(π· β
(πΌβπ) β§
πΈ β
(πΌβπ) β§
πΉ β
(πΌβπ))) β§
(π¦ β
(πΌβπ) β§
π§ β
(πΌβπ))) β§
π€ β
(πΌβπ)) β§
((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©))) β ((π€ Btwn β¨πΈ, π§β© β§ β¨πΆ, β¨π¦, π·β©β©Cgr3β¨πΈ, β¨π€, π§β©β©) β (π€ Btwn β¨πΈ, πΉβ© β§ β¨π΄, π΅β©Cgrβ¨πΈ, π€β©))) |
45 | 44 | an32s 651 |
. . . . . 6
β’
(((((π β
β β§ (π΄ β
(πΌβπ) β§
π΅ β
(πΌβπ) β§
πΆ β
(πΌβπ)) β§
(π· β
(πΌβπ) β§
πΈ β
(πΌβπ) β§
πΉ β
(πΌβπ))) β§
(π¦ β
(πΌβπ) β§
π§ β
(πΌβπ))) β§
((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©))) β§ π€ β (πΌβπ)) β ((π€ Btwn β¨πΈ, π§β© β§ β¨πΆ, β¨π¦, π·β©β©Cgr3β¨πΈ, β¨π€, π§β©β©) β (π€ Btwn β¨πΈ, πΉβ© β§ β¨π΄, π΅β©Cgrβ¨πΈ, π€β©))) |
46 | 45 | reximdva 3162 |
. . . . 5
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ))) β§ ((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©))) β (βπ€ β (πΌβπ)(π€ Btwn β¨πΈ, π§β© β§ β¨πΆ, β¨π¦, π·β©β©Cgr3β¨πΈ, β¨π€, π§β©β©) β βπ€ β (πΌβπ)(π€ Btwn β¨πΈ, πΉβ© β§ β¨π΄, π΅β©Cgrβ¨πΈ, π€β©))) |
47 | 13, 46 | mpd 15 |
. . . 4
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β§ (π¦ β (πΌβπ) β§ π§ β (πΌβπ))) β§ ((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©))) β βπ€ β (πΌβπ)(π€ Btwn β¨πΈ, πΉβ© β§ β¨π΄, π΅β©Cgrβ¨πΈ, π€β©)) |
48 | 47 | exp31 421 |
. . 3
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β ((π¦ β (πΌβπ) β§ π§ β (πΌβπ)) β (((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©)) β βπ€ β (πΌβπ)(π€ Btwn β¨πΈ, πΉβ© β§ β¨π΄, π΅β©Cgrβ¨πΈ, π€β©)))) |
49 | 48 | rexlimdvv 3201 |
. 2
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (βπ¦ β (πΌβπ)βπ§ β (πΌβπ)((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©)) β βπ€ β (πΌβπ)(π€ Btwn β¨πΈ, πΉβ© β§ β¨π΄, π΅β©Cgrβ¨πΈ, π€β©))) |
50 | | simp1 1137 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β π β β) |
51 | | simp21 1207 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β π΄ β (πΌβπ)) |
52 | | simp22 1208 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β π΅ β (πΌβπ)) |
53 | | simp23 1209 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β πΆ β (πΌβπ)) |
54 | | simp31 1210 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β π· β (πΌβπ)) |
55 | | brsegle 34739 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β (β¨π΄, π΅β© Segβ€ β¨πΆ, π·β© β βπ¦ β (πΌβπ)(π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©))) |
56 | 50, 51, 52, 53, 54, 55 | syl122anc 1380 |
. . . 4
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (β¨π΄, π΅β© Segβ€ β¨πΆ, π·β© β βπ¦ β (πΌβπ)(π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©))) |
57 | | simp32 1211 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β πΈ β (πΌβπ)) |
58 | | simp33 1212 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β πΉ β (πΌβπ)) |
59 | | brsegle 34739 |
. . . . 5
β’ ((π β β β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ (πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (β¨πΆ, π·β© Segβ€ β¨πΈ, πΉβ© β βπ§ β (πΌβπ)(π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©))) |
60 | 50, 53, 54, 57, 58, 59 | syl122anc 1380 |
. . . 4
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (β¨πΆ, π·β© Segβ€ β¨πΈ, πΉβ© β βπ§ β (πΌβπ)(π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©))) |
61 | 56, 60 | anbi12d 632 |
. . 3
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β ((β¨π΄, π΅β© Segβ€ β¨πΆ, π·β© β§ β¨πΆ, π·β© Segβ€ β¨πΈ, πΉβ©) β (βπ¦ β (πΌβπ)(π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ βπ§ β (πΌβπ)(π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©)))) |
62 | | reeanv 3216 |
. . 3
β’
(βπ¦ β
(πΌβπ)βπ§ β (πΌβπ)((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©)) β (βπ¦ β (πΌβπ)(π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ βπ§ β (πΌβπ)(π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©))) |
63 | 61, 62 | bitr4di 289 |
. 2
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β ((β¨π΄, π΅β© Segβ€ β¨πΆ, π·β© β§ β¨πΆ, π·β© Segβ€ β¨πΈ, πΉβ©) β βπ¦ β (πΌβπ)βπ§ β (πΌβπ)((π¦ Btwn β¨πΆ, π·β© β§ β¨π΄, π΅β©Cgrβ¨πΆ, π¦β©) β§ (π§ Btwn β¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, π§β©)))) |
64 | | brsegle 34739 |
. . 3
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (β¨π΄, π΅β© Segβ€ β¨πΈ, πΉβ© β βπ€ β (πΌβπ)(π€ Btwn β¨πΈ, πΉβ© β§ β¨π΄, π΅β©Cgrβ¨πΈ, π€β©))) |
65 | 50, 51, 52, 57, 58, 64 | syl122anc 1380 |
. 2
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (β¨π΄, π΅β© Segβ€ β¨πΈ, πΉβ© β βπ€ β (πΌβπ)(π€ Btwn β¨πΈ, πΉβ© β§ β¨π΄, π΅β©Cgrβ¨πΈ, π€β©))) |
66 | 49, 63, 65 | 3imtr4d 294 |
1
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β ((β¨π΄, π΅β© Segβ€ β¨πΆ, π·β© β§ β¨πΆ, π·β© Segβ€ β¨πΈ, πΉβ©) β β¨π΄, π΅β© Segβ€ β¨πΈ, πΉβ©)) |