Metamath Proof Explorer

Theorem cgrextend

Description: Link congruence over a pair of line segments. Theorem 2.11 of Schwabhauser p. 29. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion cgrextend 
|- ( ( 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 ) ) ) -> ( ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> <. A , C >. Cgr <. D , F >. ) )

Proof

Step Hyp Ref Expression
1 opeq1 
 |-  ( A = B -> <. A , B >. = <. B , B >. )
2 1 breq1d 
 |-  ( A = B -> ( <. A , B >. Cgr <. D , E >. <-> <. B , B >. Cgr <. D , E >. ) )
3 2 adantr 
 |-  ( ( A = B /\ ( 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 ) ) ) ) -> ( <. A , B >. Cgr <. D , E >. <-> <. B , B >. Cgr <. D , E >. ) )
4 simp1 
 |-  ( ( 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 ) ) ) -> N e. NN )
5 simp22 
 |-  ( ( 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 ) ) ) -> B e. ( EE ` N ) )
6 simp31 
 |-  ( ( 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 ) ) ) -> D e. ( EE ` N ) )
7 simp32 
 |-  ( ( 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 ) ) ) -> E e. ( EE ` N ) )
8 cgrid2 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( <. B , B >. Cgr <. D , E >. -> D = E ) )
9 4 5 6 7 8 syl13anc 
 |-  ( ( 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 ) ) ) -> ( <. B , B >. Cgr <. D , E >. -> D = E ) )
10 9 adantl 
 |-  ( ( A = B /\ ( 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 ) ) ) ) -> ( <. B , B >. Cgr <. D , E >. -> D = E ) )
11 3 10 sylbid 
 |-  ( ( A = B /\ ( 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 ) ) ) ) -> ( <. A , B >. Cgr <. D , E >. -> D = E ) )
12 opeq1 
 |-  ( A = B -> <. A , C >. = <. B , C >. )
13 opeq1 
 |-  ( D = E -> <. D , F >. = <. E , F >. )
14 12 13 breqan12d 
 |-  ( ( A = B /\ D = E ) -> ( <. A , C >. Cgr <. D , F >. <-> <. B , C >. Cgr <. E , F >. ) )
15 14 exbiri 
 |-  ( A = B -> ( D = E -> ( <. B , C >. Cgr <. E , F >. -> <. A , C >. Cgr <. D , F >. ) ) )
16 15 adantr 
 |-  ( ( A = B /\ ( 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 ) ) ) ) -> ( D = E -> ( <. B , C >. Cgr <. E , F >. -> <. A , C >. Cgr <. D , F >. ) ) )
17 11 16 syld 
 |-  ( ( A = B /\ ( 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 ) ) ) ) -> ( <. A , B >. Cgr <. D , E >. -> ( <. B , C >. Cgr <. E , F >. -> <. A , C >. Cgr <. D , F >. ) ) )
18 17 impd 
 |-  ( ( A = B /\ ( 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 ) ) ) ) -> ( ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) -> <. A , C >. Cgr <. D , F >. ) )
19 18 adantld 
 |-  ( ( A = B /\ ( 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 ) ) ) ) -> ( ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> <. A , C >. Cgr <. D , F >. ) )
20 19 ex 
 |-  ( A = B -> ( ( 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 ) ) ) -> ( ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> <. A , C >. Cgr <. D , F >. ) ) )
21 simpl1 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> N e. NN )
22 simpl21 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> A e. ( EE ` N ) )
23 simpl22 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> B e. ( EE ` N ) )
24 21 22 23 3jca 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) )
25 simpl23 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> C e. ( EE ` N ) )
26 simpl31 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> D e. ( EE ` N ) )
27 25 22 26 3jca 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> ( C e. ( EE ` N ) /\ A e. ( EE ` N ) /\ D e. ( EE ` N ) ) )
28 simpl32 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> E e. ( EE ` N ) )
29 simpl33 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> F e. ( EE ` N ) )
30 28 29 26 3jca 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ D e. ( EE ` N ) ) )
31 24 27 30 3jca 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ A e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) )
32 simprrl 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) )
33 simprrr 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) )
34 cgrtriv 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> <. A , A >. Cgr <. D , D >. )
35 21 22 26 34 syl3anc 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> <. A , A >. Cgr <. D , D >. )
36 33 simpld 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> <. A , B >. Cgr <. D , E >. )
37 cgrcomlr 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. D , E >. <-> <. B , A >. Cgr <. E , D >. ) )
38 21 22 23 26 28 37 syl122anc 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> ( <. A , B >. Cgr <. D , E >. <-> <. B , A >. Cgr <. E , D >. ) )
39 36 38 mpbid 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> <. B , A >. Cgr <. E , D >. )
40 35 39 jca 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> ( <. A , A >. Cgr <. D , D >. /\ <. B , A >. Cgr <. E , D >. ) )
41 brofs 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ A e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. <. A , B >. , <. C , A >. >. OuterFiveSeg <. <. D , E >. , <. F , D >. >. <-> ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) /\ ( <. A , A >. Cgr <. D , D >. /\ <. B , A >. Cgr <. E , D >. ) ) ) )
42 21 22 23 25 22 26 28 29 26 41 syl333anc 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> ( <. <. A , B >. , <. C , A >. >. OuterFiveSeg <. <. D , E >. , <. F , D >. >. <-> ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) /\ ( <. A , A >. Cgr <. D , D >. /\ <. B , A >. Cgr <. E , D >. ) ) ) )
43 32 33 40 42 mpbir3and 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> <. <. A , B >. , <. C , A >. >. OuterFiveSeg <. <. D , E >. , <. F , D >. >. )
44 simprl 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> A =/= B )
45 43 44 jca 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> ( <. <. A , B >. , <. C , A >. >. OuterFiveSeg <. <. D , E >. , <. F , D >. >. /\ A =/= B ) )
46 5segofs 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ A e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( <. <. A , B >. , <. C , A >. >. OuterFiveSeg <. <. D , E >. , <. F , D >. >. /\ A =/= B ) -> <. C , A >. Cgr <. F , D >. ) )
47 31 45 46 sylc 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> <. C , A >. Cgr <. F , D >. )
48 cgrcomlr 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. C , A >. Cgr <. F , D >. <-> <. A , C >. Cgr <. D , F >. ) )
49 21 25 22 29 26 48 syl122anc 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> ( <. C , A >. Cgr <. F , D >. <-> <. A , C >. Cgr <. D , F >. ) )
50 47 49 mpbid 
 |-  ( ( ( 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 ) ) ) /\ ( A =/= B /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) ) ) -> <. A , C >. Cgr <. D , F >. )
51 50 exp32 
 |-  ( ( 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 ) ) ) -> ( A =/= B -> ( ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> <. A , C >. Cgr <. D , F >. ) ) )
52 51 com12 
 |-  ( A =/= B -> ( ( 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 ) ) ) -> ( ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> <. A , C >. Cgr <. D , F >. ) ) )
53 20 52 pm2.61ine 
 |-  ( ( 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 ) ) ) -> ( ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> <. A , C >. Cgr <. D , F >. ) )