Metamath Proof Explorer

Theorem cgr3permute3

Description: Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013)

Ref Expression
Assertion cgr3permute3 
|- ( ( 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 , C >. >. Cgr3 <. D , <. E , F >. >. <-> <. B , <. C , A >. >. Cgr3 <. E , <. F , D >. >. ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( N e. NN -> N e. NN )
2 3simpa 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) )
3 3simpa 
 |-  ( ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) -> ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) )
4 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 >. ) )
5 1 2 3 4 syl3an 
 |-  ( ( 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 , A >. Cgr <. E , D >. ) )
6 3simpb 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
7 3simpb 
 |-  ( ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) -> ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) )
8 cgrcomlr 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. A , C >. Cgr <. D , F >. <-> <. C , A >. Cgr <. F , D >. ) )
9 1 6 7 8 syl3an 
 |-  ( ( 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 , C >. Cgr <. D , F >. <-> <. C , A >. Cgr <. F , D >. ) )
10 5 9 3anbi12d 
 |-  ( ( 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 >. /\ <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) <-> ( <. B , A >. Cgr <. E , D >. /\ <. C , A >. Cgr <. F , D >. /\ <. B , C >. Cgr <. E , F >. ) ) )
11 3anrot 
 |-  ( ( <. B , C >. Cgr <. E , F >. /\ <. B , A >. Cgr <. E , D >. /\ <. C , A >. Cgr <. F , D >. ) <-> ( <. B , A >. Cgr <. E , D >. /\ <. C , A >. Cgr <. F , D >. /\ <. B , C >. Cgr <. E , F >. ) )
12 10 11 bitr4di 
 |-  ( ( 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 >. /\ <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) <-> ( <. B , C >. Cgr <. E , F >. /\ <. B , A >. Cgr <. E , D >. /\ <. C , A >. Cgr <. F , D >. ) ) )
13 brcgr3 
 |-  ( ( 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 , C >. >. Cgr3 <. D , <. E , F >. >. <-> ( <. A , B >. Cgr <. D , E >. /\ <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) )
14 biid 
 |-  ( N e. NN <-> N e. NN )
15 3anrot 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) <-> ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) )
16 3anrot 
 |-  ( ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) <-> ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ D e. ( EE ` N ) ) )
17 brcgr3 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. B , <. C , A >. >. Cgr3 <. E , <. F , D >. >. <-> ( <. B , C >. Cgr <. E , F >. /\ <. B , A >. Cgr <. E , D >. /\ <. C , A >. Cgr <. F , D >. ) ) )
18 14 15 16 17 syl3anb 
 |-  ( ( 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 , <. C , A >. >. Cgr3 <. E , <. F , D >. >. <-> ( <. B , C >. Cgr <. E , F >. /\ <. B , A >. Cgr <. E , D >. /\ <. C , A >. Cgr <. F , D >. ) ) )
19 12 13 18 3bitr4d 
 |-  ( ( 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 , C >. >. Cgr3 <. D , <. E , F >. >. <-> <. B , <. C , A >. >. Cgr3 <. E , <. F , D >. >. ) )