Metamath Proof Explorer


Theorem cgr3permute2

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

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

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