Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . . 5
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β π β β) |
2 | | simpl23 1254 |
. . . . . 6
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β πΆ β (πΌβπ)) |
3 | | simpl21 1252 |
. . . . . 6
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β π΄ β (πΌβπ)) |
4 | | simpl31 1255 |
. . . . . 6
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β π· β (πΌβπ)) |
5 | 2, 3, 4 | 3jca 1129 |
. . . . 5
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β (πΆ β (πΌβπ) β§ π΄ β (πΌβπ) β§ π· β (πΌβπ))) |
6 | | simpl32 1256 |
. . . . . 6
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β πΈ β (πΌβπ)) |
7 | | simpl33 1257 |
. . . . . 6
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β π β (πΌβπ)) |
8 | 6, 7 | jca 513 |
. . . . 5
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β (πΈ β (πΌβπ) β§ π β (πΌβπ))) |
9 | 1, 5, 8 | 3jca 1129 |
. . . 4
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β (π β β β§ (πΆ β (πΌβπ) β§ π΄ β (πΌβπ) β§ π· β (πΌβπ)) β§ (πΈ β (πΌβπ) β§ π β (πΌβπ)))) |
10 | | simpr2 1196 |
. . . . . 6
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β πΈ Btwn β¨π·, πΆβ©) |
11 | | btwncom 34645 |
. . . . . . 7
β’ ((π β β β§ (πΈ β (πΌβπ) β§ π· β (πΌβπ) β§ πΆ β (πΌβπ))) β (πΈ Btwn β¨π·, πΆβ© β πΈ Btwn β¨πΆ, π·β©)) |
12 | 1, 6, 4, 2, 11 | syl13anc 1373 |
. . . . . 6
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β (πΈ Btwn β¨π·, πΆβ© β πΈ Btwn β¨πΆ, π·β©)) |
13 | 10, 12 | mpbid 231 |
. . . . 5
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β πΈ Btwn β¨πΆ, π·β©) |
14 | | simpr3 1197 |
. . . . 5
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β π Btwn β¨π΄, π·β©) |
15 | 13, 14 | jca 513 |
. . . 4
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β (πΈ Btwn β¨πΆ, π·β© β§ π Btwn β¨π΄, π·β©)) |
16 | | axpasch 27932 |
. . . 4
β’ ((π β β β§ (πΆ β (πΌβπ) β§ π΄ β (πΌβπ) β§ π· β (πΌβπ)) β§ (πΈ β (πΌβπ) β§ π β (πΌβπ))) β ((πΈ Btwn β¨πΆ, π·β© β§ π Btwn β¨π΄, π·β©) β βπ β (πΌβπ)(π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©))) |
17 | 9, 15, 16 | sylc 65 |
. . 3
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β βπ β (πΌβπ)(π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) |
18 | | simp1l1 1267 |
. . . . . . 7
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β π β β) |
19 | 6 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β πΈ β (πΌβπ)) |
20 | 2 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β πΆ β (πΌβπ)) |
21 | 3 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β π΄ β (πΌβπ)) |
22 | 19, 20, 21 | 3jca 1129 |
. . . . . . 7
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β (πΈ β (πΌβπ) β§ πΆ β (πΌβπ) β§ π΄ β (πΌβπ))) |
23 | | simp2 1138 |
. . . . . . . 8
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β π β (πΌβπ)) |
24 | | simpl22 1253 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β π΅ β (πΌβπ)) |
25 | 24 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β π΅ β (πΌβπ)) |
26 | 23, 25 | jca 513 |
. . . . . . 7
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β (π β (πΌβπ) β§ π΅ β (πΌβπ))) |
27 | 18, 22, 26 | 3jca 1129 |
. . . . . 6
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β (π β β β§ (πΈ β (πΌβπ) β§ πΆ β (πΌβπ) β§ π΄ β (πΌβπ)) β§ (π β (πΌβπ) β§ π΅ β (πΌβπ)))) |
28 | | simp3l 1202 |
. . . . . . 7
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β π Btwn β¨πΈ, π΄β©) |
29 | | simp1r1 1270 |
. . . . . . . 8
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β π΅ Btwn β¨π΄, πΆβ©) |
30 | | btwncom 34645 |
. . . . . . . . 9
β’ ((π β β β§ (π΅ β (πΌβπ) β§ π΄ β (πΌβπ) β§ πΆ β (πΌβπ))) β (π΅ Btwn β¨π΄, πΆβ© β π΅ Btwn β¨πΆ, π΄β©)) |
31 | 18, 25, 21, 20, 30 | syl13anc 1373 |
. . . . . . . 8
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β (π΅ Btwn β¨π΄, πΆβ© β π΅ Btwn β¨πΆ, π΄β©)) |
32 | 29, 31 | mpbid 231 |
. . . . . . 7
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β π΅ Btwn β¨πΆ, π΄β©) |
33 | 28, 32 | jca 513 |
. . . . . 6
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β (π Btwn β¨πΈ, π΄β© β§ π΅ Btwn β¨πΆ, π΄β©)) |
34 | | axpasch 27932 |
. . . . . 6
β’ ((π β β β§ (πΈ β (πΌβπ) β§ πΆ β (πΌβπ) β§ π΄ β (πΌβπ)) β§ (π β (πΌβπ) β§ π΅ β (πΌβπ))) β ((π Btwn β¨πΈ, π΄β© β§ π΅ Btwn β¨πΆ, π΄β©) β βπ β (πΌβπ)(π Btwn β¨π, πΆβ© β§ π Btwn β¨π΅, πΈβ©))) |
35 | 27, 33, 34 | sylc 65 |
. . . . 5
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β βπ β (πΌβπ)(π Btwn β¨π, πΆβ© β§ π Btwn β¨π΅, πΈβ©)) |
36 | | simpll1 1213 |
. . . . . . . . . . 11
β’
((((((π β
β β§ (π΄ β
(πΌβπ) β§
π΅ β
(πΌβπ) β§
πΆ β
(πΌβπ)) β§
(π· β
(πΌβπ) β§
πΈ β
(πΌβπ) β§
π β
(πΌβπ))) β§
(π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β§ π β (πΌβπ)) β§ π Btwn β¨π, πΆβ©) β ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©))) |
37 | 36, 1 | syl 17 |
. . . . . . . . . 10
β’
((((((π β
β β§ (π΄ β
(πΌβπ) β§
π΅ β
(πΌβπ) β§
πΆ β
(πΌβπ)) β§
(π· β
(πΌβπ) β§
πΈ β
(πΌβπ) β§
π β
(πΌβπ))) β§
(π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β§ π β (πΌβπ)) β§ π Btwn β¨π, πΆβ©) β π β β) |
38 | 36, 7 | syl 17 |
. . . . . . . . . . 11
β’
((((((π β
β β§ (π΄ β
(πΌβπ) β§
π΅ β
(πΌβπ) β§
πΆ β
(πΌβπ)) β§
(π· β
(πΌβπ) β§
πΈ β
(πΌβπ) β§
π β
(πΌβπ))) β§
(π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β§ π β (πΌβπ)) β§ π Btwn β¨π, πΆβ©) β π β (πΌβπ)) |
39 | | simpll2 1214 |
. . . . . . . . . . 11
β’
((((((π β
β β§ (π΄ β
(πΌβπ) β§
π΅ β
(πΌβπ) β§
πΆ β
(πΌβπ)) β§
(π· β
(πΌβπ) β§
πΈ β
(πΌβπ) β§
π β
(πΌβπ))) β§
(π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β§ π β (πΌβπ)) β§ π Btwn β¨π, πΆβ©) β π β (πΌβπ)) |
40 | 38, 39 | jca 513 |
. . . . . . . . . 10
β’
((((((π β
β β§ (π΄ β
(πΌβπ) β§
π΅ β
(πΌβπ) β§
πΆ β
(πΌβπ)) β§
(π· β
(πΌβπ) β§
πΈ β
(πΌβπ) β§
π β
(πΌβπ))) β§
(π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β§ π β (πΌβπ)) β§ π Btwn β¨π, πΆβ©) β (π β (πΌβπ) β§ π β (πΌβπ))) |
41 | | simplr 768 |
. . . . . . . . . . 11
β’
((((((π β
β β§ (π΄ β
(πΌβπ) β§
π΅ β
(πΌβπ) β§
πΆ β
(πΌβπ)) β§
(π· β
(πΌβπ) β§
πΈ β
(πΌβπ) β§
π β
(πΌβπ))) β§
(π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β§ π β (πΌβπ)) β§ π Btwn β¨π, πΆβ©) β π β (πΌβπ)) |
42 | 36, 2 | syl 17 |
. . . . . . . . . . 11
β’
((((((π β
β β§ (π΄ β
(πΌβπ) β§
π΅ β
(πΌβπ) β§
πΆ β
(πΌβπ)) β§
(π· β
(πΌβπ) β§
πΈ β
(πΌβπ) β§
π β
(πΌβπ))) β§
(π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β§ π β (πΌβπ)) β§ π Btwn β¨π, πΆβ©) β πΆ β (πΌβπ)) |
43 | 41, 42 | jca 513 |
. . . . . . . . . 10
β’
((((((π β
β β§ (π΄ β
(πΌβπ) β§
π΅ β
(πΌβπ) β§
πΆ β
(πΌβπ)) β§
(π· β
(πΌβπ) β§
πΈ β
(πΌβπ) β§
π β
(πΌβπ))) β§
(π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β§ π β (πΌβπ)) β§ π Btwn β¨π, πΆβ©) β (π β (πΌβπ) β§ πΆ β (πΌβπ))) |
44 | 37, 40, 43 | 3jca 1129 |
. . . . . . . . 9
β’
((((((π β
β β§ (π΄ β
(πΌβπ) β§
π΅ β
(πΌβπ) β§
πΆ β
(πΌβπ)) β§
(π· β
(πΌβπ) β§
πΈ β
(πΌβπ) β§
π β
(πΌβπ))) β§
(π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β§ π β (πΌβπ)) β§ π Btwn β¨π, πΆβ©) β (π β β β§ (π β (πΌβπ) β§ π β (πΌβπ)) β§ (π β (πΌβπ) β§ πΆ β (πΌβπ)))) |
45 | | simpl3r 1230 |
. . . . . . . . . 10
β’
(((((π β
β β§ (π΄ β
(πΌβπ) β§
π΅ β
(πΌβπ) β§
πΆ β
(πΌβπ)) β§
(π· β
(πΌβπ) β§
πΈ β
(πΌβπ) β§
π β
(πΌβπ))) β§
(π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β§ π β (πΌβπ)) β π Btwn β¨π, πΆβ©) |
46 | 45 | anim1i 616 |
. . . . . . . . 9
β’
((((((π β
β β§ (π΄ β
(πΌβπ) β§
π΅ β
(πΌβπ) β§
πΆ β
(πΌβπ)) β§
(π· β
(πΌβπ) β§
πΈ β
(πΌβπ) β§
π β
(πΌβπ))) β§
(π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β§ π β (πΌβπ)) β§ π Btwn β¨π, πΆβ©) β (π Btwn β¨π, πΆβ© β§ π Btwn β¨π, πΆβ©)) |
47 | | btwnexch2 34654 |
. . . . . . . . 9
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ)) β§ (π β (πΌβπ) β§ πΆ β (πΌβπ))) β ((π Btwn β¨π, πΆβ© β§ π Btwn β¨π, πΆβ©) β π Btwn β¨π, πΆβ©)) |
48 | 44, 46, 47 | sylc 65 |
. . . . . . . 8
β’
((((((π β
β β§ (π΄ β
(πΌβπ) β§
π΅ β
(πΌβπ) β§
πΆ β
(πΌβπ)) β§
(π· β
(πΌβπ) β§
πΈ β
(πΌβπ) β§
π β
(πΌβπ))) β§
(π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β§ π β (πΌβπ)) β§ π Btwn β¨π, πΆβ©) β π Btwn β¨π, πΆβ©) |
49 | 48 | ex 414 |
. . . . . . 7
β’
(((((π β
β β§ (π΄ β
(πΌβπ) β§
π΅ β
(πΌβπ) β§
πΆ β
(πΌβπ)) β§
(π· β
(πΌβπ) β§
πΈ β
(πΌβπ) β§
π β
(πΌβπ))) β§
(π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β§ π β (πΌβπ)) β (π Btwn β¨π, πΆβ© β π Btwn β¨π, πΆβ©)) |
50 | 49 | anim1d 612 |
. . . . . 6
β’
(((((π β
β β§ (π΄ β
(πΌβπ) β§
π΅ β
(πΌβπ) β§
πΆ β
(πΌβπ)) β§
(π· β
(πΌβπ) β§
πΈ β
(πΌβπ) β§
π β
(πΌβπ))) β§
(π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β§ π β (πΌβπ)) β ((π Btwn β¨π, πΆβ© β§ π Btwn β¨π΅, πΈβ©) β (π Btwn β¨π, πΆβ© β§ π Btwn β¨π΅, πΈβ©))) |
51 | 50 | reximdva 3162 |
. . . . 5
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β (βπ β (πΌβπ)(π Btwn β¨π, πΆβ© β§ π Btwn β¨π΅, πΈβ©) β βπ β (πΌβπ)(π Btwn β¨π, πΆβ© β§ π Btwn β¨π΅, πΈβ©))) |
52 | 35, 51 | mpd 15 |
. . . 4
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β§ π β (πΌβπ) β§ (π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©)) β βπ β (πΌβπ)(π Btwn β¨π, πΆβ© β§ π Btwn β¨π΅, πΈβ©)) |
53 | 52 | rexlimdv3a 3153 |
. . 3
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β (βπ β (πΌβπ)(π Btwn β¨πΈ, π΄β© β§ π Btwn β¨π, πΆβ©) β βπ β (πΌβπ)(π Btwn β¨π, πΆβ© β§ π Btwn β¨π΅, πΈβ©))) |
54 | 17, 53 | mpd 15 |
. 2
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β§ (π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©)) β βπ β (πΌβπ)(π Btwn β¨π, πΆβ© β§ π Btwn β¨π΅, πΈβ©)) |
55 | 54 | ex 414 |
1
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ π β (πΌβπ))) β ((π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΆβ© β§ π Btwn β¨π΄, π·β©) β βπ β (πΌβπ)(π Btwn β¨π, πΆβ© β§ π Btwn β¨π΅, πΈβ©))) |