Metamath Proof Explorer

Theorem cgr3permute1

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

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

Proof

Step Hyp Ref Expression
1 id 
 |-  ( N e. NN -> N e. NN )
2 3simpc 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
3 3simpc 
 |-  ( ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) -> ( E e. ( EE ` N ) /\ F e. ( EE ` N ) ) )
4 cgrcomlr 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. B , C >. Cgr <. E , F >. <-> <. C , B >. Cgr <. F , E >. ) )
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 ) ) ) -> ( <. B , C >. Cgr <. E , F >. <-> <. C , B >. Cgr <. F , E >. ) )
6 5 3anbi3d 
 |-  ( ( 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 >. ) <-> ( <. A , B >. Cgr <. D , E >. /\ <. A , C >. Cgr <. D , F >. /\ <. C , B >. Cgr <. F , E >. ) ) )
7 3ancoma 
 |-  ( ( <. A , B >. Cgr <. D , E >. /\ <. A , C >. Cgr <. D , F >. /\ <. C , B >. Cgr <. F , E >. ) <-> ( <. A , C >. Cgr <. D , F >. /\ <. A , B >. Cgr <. D , E >. /\ <. C , B >. Cgr <. F , E >. ) )
8 6 7 bitrdi 
 |-  ( ( 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 >. ) <-> ( <. A , C >. Cgr <. D , F >. /\ <. A , B >. Cgr <. D , E >. /\ <. C , B >. Cgr <. F , E >. ) ) )
9 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 >. ) ) )
10 biid 
 |-  ( N e. NN <-> N e. NN )
11 3ancomb 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) <-> ( A e. ( EE ` N ) /\ C e. ( EE ` N ) /\ B e. ( EE ` N ) ) )
12 3ancomb 
 |-  ( ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) <-> ( D e. ( EE ` N ) /\ F e. ( EE ` N ) /\ E e. ( EE ` N ) ) )
13 brcgr3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( <. A , <. C , B >. >. Cgr3 <. D , <. F , E >. >. <-> ( <. A , C >. Cgr <. D , F >. /\ <. A , B >. Cgr <. D , E >. /\ <. C , B >. Cgr <. F , E >. ) ) )
14 10 11 12 13 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 ) ) ) -> ( <. A , <. C , B >. >. Cgr3 <. D , <. F , E >. >. <-> ( <. A , C >. Cgr <. D , F >. /\ <. A , B >. Cgr <. D , E >. /\ <. C , B >. Cgr <. F , E >. ) ) )
15 8 9 14 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 >. >. <-> <. A , <. C , B >. >. Cgr3 <. D , <. F , E >. >. ) )