Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ifscgr Structured version   Visualization version   Unicode version
Theorem ifscgr 30859
Description: Inner five segment congruence. Take two triangles, A D C and E H G, with B between A and C and F between E and G. If the other components of the triangles are congruent, then so are B D and F H. Theorem 4.2 of [Schwabhauser] p. 34. (Contributed by Scott Fenton, 27-Sep-2013.)
Assertion
Ref Expression
ifscgr |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , B >. , <. C , D >. >. InnerFiveSeg <. <. E , F >. , <. G , H >. >. -> <. B , D >.Cgr <. F , H >. ) )
Proof of Theorem ifscgr
Dummy variables e f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 brifs 30858 . 2 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , B >. , <. C , D >. >. InnerFiveSeg <. <. E , F >. , <. G , H >. >. <-> ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) )
2 simp1l 1038 . . . . . 6 |- ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) -> B Btwn <. C , C >. )
3 simp11 1044 . . . . . . 7 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> N e. NN )
4 simp13 1046 . . . . . . 7 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
5 simp21 1047 . . . . . . 7 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
6 axbtwnid 25017 . . . . . . 7 |- ( ( N e. NN /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( B Btwn <. C , C >. -> B = C ) )
73, 4, 5, 6syl3anc 1276 . . . . . 6 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( B Btwn <. C , C >. -> B = C ) )
82, 7syl5 33 . . . . 5 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) -> B = C ) )
9 simp2r 1041 . . . . . . . . 9 |- ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) -> <. B , C >.Cgr <. F , G >. )
10 simp3r 1043 . . . . . . . . 9 |- ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) -> <. C , D >.Cgr <. G , H >. )
119, 10jca 539 . . . . . . . 8 |- ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) -> ( <. B , C >.Cgr <. F , G >. /\ <. C , D >.Cgr <. G , H >. ) )
12 opeq2 4180 . . . . . . . . . . 11 |- ( B = C -> <. B , B >. = <. B , C >. )
1312breq1d 4425 . . . . . . . . . 10 |- ( B = C -> ( <. B , B >.Cgr <. F , G >. <-> <. B , C >.Cgr <. F , G >. ) )
14 opeq1 4179 . . . . . . . . . . 11 |- ( B = C -> <. B , D >. = <. C , D >. )
1514breq1d 4425 . . . . . . . . . 10 |- ( B = C -> ( <. B , D >.Cgr <. G , H >. <-> <. C , D >.Cgr <. G , H >. ) )
1613, 15anbi12d 722 . . . . . . . . 9 |- ( B = C -> ( ( <. B , B >.Cgr <. F , G >. /\ <. B , D >.Cgr <. G , H >. ) <-> ( <. B , C >.Cgr <. F , G >. /\ <. C , D >.Cgr <. G , H >. ) ) )
1716biimprd 231 . . . . . . . 8 |- ( B = C -> ( ( <. B , C >.Cgr <. F , G >. /\ <. C , D >.Cgr <. G , H >. ) -> ( <. B , B >.Cgr <. F , G >. /\ <. B , D >.Cgr <. G , H >. ) ) )
1811, 17mpan9 476 . . . . . . 7 |- ( ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) /\ B = C ) -> ( <. B , B >.Cgr <. F , G >. /\ <. B , D >.Cgr <. G , H >. ) )
19 simp31 1050 . . . . . . . . . 10 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> F e. ( EE ` N ) )
20 simp32 1051 . . . . . . . . . 10 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> G e. ( EE ` N ) )
21 cgrid2 30818 . . . . . . . . . 10 |- ( ( N e. NN /\ ( B e. ( EE ` N ) /\ F e. ( EE ` N ) /\ G e. ( EE ` N ) ) ) -> ( <. B , B >.Cgr <. F , G >. -> F = G ) )
223, 4, 19, 20, 21syl13anc 1278 . . . . . . . . 9 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. B , B >.Cgr <. F , G >. -> F = G ) )
23 opeq1 4179 . . . . . . . . . . 11 |- ( F = G -> <. F , H >. = <. G , H >. )
2423breq2d 4427 . . . . . . . . . 10 |- ( F = G -> ( <. B , D >.Cgr <. F , H >. <-> <. B , D >.Cgr <. G , H >. ) )
2524biimprd 231 . . . . . . . . 9 |- ( F = G -> ( <. B , D >.Cgr <. G , H >. -> <. B , D >.Cgr <. F , H >. ) )
2622, 25syl6 34 . . . . . . . 8 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. B , B >.Cgr <. F , G >. -> ( <. B , D >.Cgr <. G , H >. -> <. B , D >.Cgr <. F , H >. ) ) )
2726impd 437 . . . . . . 7 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. B , B >.Cgr <. F , G >. /\ <. B , D >.Cgr <. G , H >. ) -> <. B , D >.Cgr <. F , H >. ) )
2818, 27syl5 33 . . . . . 6 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) /\ B = C ) -> <. B , D >.Cgr <. F , H >. ) )
2928expd 442 . . . . 5 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) -> ( B = C -> <. B , D >.Cgr <. F , H >. ) ) )
308, 29mpdd 41 . . . 4 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) -> <. B , D >.Cgr <. F , H >. ) )
31 opeq1 4179 . . . . . . . 8 |- ( A = C -> <. A , C >. = <. C , C >. )
3231breq2d 4427 . . . . . . 7 |- ( A = C -> ( B Btwn <. A , C >. <-> B Btwn <. C , C >. ) )
3332anbi1d 716 . . . . . 6 |- ( A = C -> ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) <-> ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) ) )
3431breq1d 4425 . . . . . . 7 |- ( A = C -> ( <. A , C >.Cgr <. E , G >. <-> <. C , C >.Cgr <. E , G >. ) )
3534anbi1d 716 . . . . . 6 |- ( A = C -> ( ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) <-> ( <. C , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) ) )
3633, 353anbi12d 1349 . . . . 5 |- ( A = C -> ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) <-> ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) )
3736imbi1d 323 . . . 4 |- ( A = C -> ( ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) -> <. B , D >.Cgr <. F , H >. ) <-> ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) -> <. B , D >.Cgr <. F , H >. ) ) )
3830, 37syl5ibr 229 . . 3 |- ( A = C -> ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) -> <. B , D >.Cgr <. F , H >. ) ) )
39 simp12 1045 . . . . . . 7 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
40 btwndiff 30842 . . . . . . 7 |- ( ( N e. NN /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> E. e e. ( EE ` N ) ( C Btwn <. A , e >. /\ C =/= e ) )
413, 39, 5, 40syl3anc 1276 . . . . . 6 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> E. e e. ( EE ` N ) ( C Btwn <. A , e >. /\ C =/= e ) )
42 simpl11 1089 . . . . . . . . . 10 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ e e. ( EE ` N ) ) -> N e. NN )
43 simpl23 1094 . . . . . . . . . 10 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ e e. ( EE ` N ) ) -> E e. ( EE ` N ) )
44 simpl32 1096 . . . . . . . . . 10 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ e e. ( EE ` N ) ) -> G e. ( EE ` N ) )
45 simpl21 1092 . . . . . . . . . 10 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ e e. ( EE ` N ) ) -> C e. ( EE ` N ) )
46 simpr 467 . . . . . . . . . 10 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ e e. ( EE ` N ) ) -> e e. ( EE ` N ) )
47 axsegcon 25005 . . . . . . . . . 10 |- ( ( N e. NN /\ ( E e. ( EE ` N ) /\ G e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ e e. ( EE ` N ) ) ) -> E. f e. ( EE ` N ) ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) )
4842, 43, 44, 45, 46, 47syl122anc 1285 . . . . . . . . 9 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ e e. ( EE ` N ) ) -> E. f e. ( EE ` N ) ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) )
49 anass 659 . . . . . . . . . . . . 13 |- ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) /\ A =/= C ) ) <-> ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( ( C Btwn <. A , e >. /\ C =/= e ) /\ ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) /\ A =/= C ) ) ) )
50 anass 659 . . . . . . . . . . . . . 14 |- ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ A =/= C ) <-> ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) /\ A =/= C ) ) )
51 simplrl 775 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) -> C Btwn <. A , e >. )
5251adantl 472 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) ) -> C Btwn <. A , e >. )
53 simplll 773 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) -> G Btwn <. E , f >. )
5453adantl 472 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) ) -> G Btwn <. E , f >. )
5552, 54jca 539 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) ) -> ( C Btwn <. A , e >. /\ G Btwn <. E , f >. ) )
56 simpr2l 1073 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) -> <. A , C >.Cgr <. E , G >. )
5756adantl 472 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) ) -> <. A , C >.Cgr <. E , G >. )
58 simpllr 774 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) -> <. G , f >.Cgr <. C , e >. )
5958adantl 472 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) ) -> <. G , f >.Cgr <. C , e >. )
603ad2antrr 737 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) ) -> N e. NN )
6120ad2antrr 737 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) ) -> G e. ( EE ` N ) )
62 simplrr 776 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) ) -> f e. ( EE ` N ) )
635ad2antrr 737 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) ) -> C e. ( EE ` N ) )
64 simplrl 775 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) ) -> e e. ( EE ` N ) )
65 cgrcom 30805 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( N e. NN /\ ( G e. ( EE ` N ) /\ f e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ e e. ( EE ` N ) ) ) -> ( <. G , f >.Cgr <. C , e >. <-> <. C , e >.Cgr <. G , f >. ) )
6660, 61, 62, 63, 64, 65syl122anc 1285 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) ) -> ( <. G , f >.Cgr <. C , e >. <-> <. C , e >.Cgr <. G , f >. ) )
6759, 66mpbid 215 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) ) -> <. C , e >.Cgr <. G , f >. )
6857, 67jca 539 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) ) -> ( <. A , C >.Cgr <. E , G >. /\ <. C , e >.Cgr <. G , f >. ) )
69 simprr3 1064 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) ) -> ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) )
7055, 68, 693jca 1194 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) ) -> ( ( C Btwn <. A , e >. /\ G Btwn <. E , f >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. C , e >.Cgr <. G , f >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) )
7170ex 440 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) -> ( ( C Btwn <. A , e >. /\ G Btwn <. E , f >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. C , e >.Cgr <. G , f >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) )
72 simpl11 1089 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> N e. NN )
73 simpl12 1090 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
74 simpl21 1092 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
75 simprl 769 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> e e. ( EE ` N ) )
76 simpl22 1093 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
77 simpl23 1094 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> E e. ( EE ` N ) )
78 simpl32 1096 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> G e. ( EE ` N ) )
79 simprr 771 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> f e. ( EE ` N ) )
80 simpl33 1097 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> H e. ( EE ` N ) )
81 brofs 30820 . . . . . . . . . . . . . . . . . 18 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( e e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ f e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , C >. , <. e , D >. >. OuterFiveSeg <. <. E , G >. , <. f , H >. >. <-> ( ( C Btwn <. A , e >. /\ G Btwn <. E , f >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. C , e >.Cgr <. G , f >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) )
8272, 73, 74, 75, 76, 77, 78, 79, 80, 81syl333anc 1308 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( <. <. A , C >. , <. e , D >. >. OuterFiveSeg <. <. E , G >. , <. f , H >. >. <-> ( ( C Btwn <. A , e >. /\ G Btwn <. E , f >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. C , e >.Cgr <. G , f >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) )
8371, 82sylibrd 242 . . . . . . . . . . . . . . . 16 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) -> <. <. A , C >. , <. e , D >. >. OuterFiveSeg <. <. E , G >. , <. f , H >. >. ) )
84 5segofs 30821 . . . . . . . . . . . . . . . . 17 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( e e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ f e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. <. A , C >. , <. e , D >. >. OuterFiveSeg <. <. E , G >. , <. f , H >. >. /\ A =/= C ) -> <. e , D >.Cgr <. f , H >. ) )
8572, 73, 74, 75, 76, 77, 78, 79, 80, 84syl333anc 1308 . . . . . . . . . . . . . . . 16 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( <. <. A , C >. , <. e , D >. >. OuterFiveSeg <. <. E , G >. , <. f , H >. >. /\ A =/= C ) -> <. e , D >.Cgr <. f , H >. ) )
8683, 85syland 488 . . . . . . . . . . . . . . 15 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ A =/= C ) -> <. e , D >.Cgr <. f , H >. ) )
87 simpr1l 1071 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) -> B Btwn <. A , C >. )
8887adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ <. e , D >.Cgr <. f , H >. ) -> B Btwn <. A , C >. )
8951adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ <. e , D >.Cgr <. f , H >. ) -> C Btwn <. A , e >. )
9088, 89jca 539 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ <. e , D >.Cgr <. f , H >. ) -> ( B Btwn <. A , C >. /\ C Btwn <. A , e >. ) )
91 simpr1r 1072 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) -> F Btwn <. E , G >. )
9291adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ <. e , D >.Cgr <. f , H >. ) -> F Btwn <. E , G >. )
9353adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ <. e , D >.Cgr <. f , H >. ) -> G Btwn <. E , f >. )
9490, 92, 93jca32 542 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ <. e , D >.Cgr <. f , H >. ) -> ( ( B Btwn <. A , C >. /\ C Btwn <. A , e >. ) /\ ( F Btwn <. E , G >. /\ G Btwn <. E , f >. ) ) )
95 simpl13 1091 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
96 btwnexch3 30835 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ e e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ C Btwn <. A , e >. ) -> C Btwn <. B , e >. ) )
9772, 73, 95, 74, 75, 96syl122anc 1285 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ C Btwn <. A , e >. ) -> C Btwn <. B , e >. ) )
98 simpl31 1095 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> F e. ( EE ` N ) )
99 btwnexch3 30835 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( N e. NN /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( F Btwn <. E , G >. /\ G Btwn <. E , f >. ) -> G Btwn <. F , f >. ) )
10072, 77, 98, 78, 79, 99syl122anc 1285 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( F Btwn <. E , G >. /\ G Btwn <. E , f >. ) -> G Btwn <. F , f >. ) )
10197, 100anim12d 570 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. A , C >. /\ C Btwn <. A , e >. ) /\ ( F Btwn <. E , G >. /\ G Btwn <. E , f >. ) ) -> ( C Btwn <. B , e >. /\ G Btwn <. F , f >. ) ) )
10294, 101syl5 33 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ <. e , D >.Cgr <. f , H >. ) -> ( C Btwn <. B , e >. /\ G Btwn <. F , f >. ) ) )
103102imp 435 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ <. e , D >.Cgr <. f , H >. ) ) -> ( C Btwn <. B , e >. /\ G Btwn <. F , f >. ) )
104 btwncom 30829 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( N e. NN /\ ( C e. ( EE ` N ) /\ B e. ( EE ` N ) /\ e e. ( EE ` N ) ) ) -> ( C Btwn <. B , e >. <-> C Btwn <. e , B >. ) )
10572, 74, 95, 75, 104syl13anc 1278 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( C Btwn <. B , e >. <-> C Btwn <. e , B >. ) )
106 btwncom 30829 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( N e. NN /\ ( G e. ( EE ` N ) /\ F e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( G Btwn <. F , f >. <-> G Btwn <. f , F >. ) )
10772, 78, 98, 79, 106syl13anc 1278 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( G Btwn <. F , f >. <-> G Btwn <. f , F >. ) )
108105, 107anbi12d 722 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( C Btwn <. B , e >. /\ G Btwn <. F , f >. ) <-> ( C Btwn <. e , B >. /\ G Btwn <. f , F >. ) ) )
109108adantr 471 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ <. e , D >.Cgr <. f , H >. ) ) -> ( ( C Btwn <. B , e >. /\ G Btwn <. F , f >. ) <-> ( C Btwn <. e , B >. /\ G Btwn <. f , F >. ) ) )
110103, 109mpbid 215 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ <. e , D >.Cgr <. f , H >. ) ) -> ( C Btwn <. e , B >. /\ G Btwn <. f , F >. ) )
11158ad2antrl 739 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ <. e , D >.Cgr <. f , H >. ) ) -> <. G , f >.Cgr <. C , e >. )
11272, 78, 79, 74, 75, 65syl122anc 1285 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( <. G , f >.Cgr <. C , e >. <-> <. C , e >.Cgr <. G , f >. ) )
113 cgrcomlr 30813 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( N e. NN /\ ( C e. ( EE ` N ) /\ e e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( <. C , e >.Cgr <. G , f >. <-> <. e , C >.Cgr <. f , G >. ) )
11472, 74, 75, 78, 79, 113syl122anc 1285 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( <. C , e >.Cgr <. G , f >. <-> <. e , C >.Cgr <. f , G >. ) )
115112, 114bitrd 261 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( <. G , f >.Cgr <. C , e >. <-> <. e , C >.Cgr <. f , G >. ) )
116115adantr 471 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ <. e , D >.Cgr <. f , H >. ) ) -> ( <. G , f >.Cgr <. C , e >. <-> <. e , C >.Cgr <. f , G >. ) )
117111, 116mpbid 215 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ <. e , D >.Cgr <. f , H >. ) ) -> <. e , C >.Cgr <. f , G >. )
118 simpr2r 1074 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) -> <. B , C >.Cgr <. F , G >. )
119118ad2antrl 739 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ <. e , D >.Cgr <. f , H >. ) ) -> <. B , C >.Cgr <. F , G >. )
12072, 95, 74, 98, 78, 119cgrcomlrand 30816 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ <. e , D >.Cgr <. f , H >. ) ) -> <. C , B >.Cgr <. G , F >. )
121117, 120jca 539 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ <. e , D >.Cgr <. f , H >. ) ) -> ( <. e , C >.Cgr <. f , G >. /\ <. C , B >.Cgr <. G , F >. ) )
122 simprr 771 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ <. e , D >.Cgr <. f , H >. ) ) -> <. e , D >.Cgr <. f , H >. )
123 simpr3r 1076 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) -> <. C , D >.Cgr <. G , H >. )
124123ad2antrl 739 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ <. e , D >.Cgr <. f , H >. ) ) -> <. C , D >.Cgr <. G , H >. )
125122, 124jca 539 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >.Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >.Cgr <. E , G >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. C , D >.Cgr <. G , H >. ) ) ) /\ <. e ,