Metamath Proof Explorer

Theorem cgr3permute4

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

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

Proof

Step Hyp Ref Expression
1 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 >. >. ) )
2 biid 
 |-  ( N e. NN <-> N e. NN )
3 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 ) ) )
4 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 ) ) )
5 cgr3permute3 
 |-  ( ( 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 >. >. <-> <. C , <. A , B >. >. Cgr3 <. F , <. D , E >. >. ) )
6 2 3 4 5 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 >. >. <-> <. C , <. A , B >. >. Cgr3 <. F , <. D , E >. >. ) )
7 1 6 bitrd 
 |-  ( ( 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 >. >. <-> <. C , <. A , B >. >. Cgr3 <. F , <. D , E >. >. ) )