Metamath Proof Explorer

Theorem cgr3com

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

Ref

Expression

Assertion

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

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		cgrcom	\|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. D , E >. <-> <. D , E >. Cgr <. A , B >. ) )
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 >. <-> <. D , E >. Cgr <. A , B >. ) )
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		cgrcom	\|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. A , C >. Cgr <. D , F >. <-> <. D , F >. Cgr <. A , C >. ) )
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 >. <-> <. D , F >. Cgr <. A , C >. ) )
10		3simpc	\|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
11		3simpc	\|- ( ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) -> ( E e. ( EE ` N ) /\ F e. ( EE ` N ) ) )
12		cgrcom	\|- ( ( N e. NN /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. B , C >. Cgr <. E , F >. <-> <. E , F >. Cgr <. B , C >. ) )
13	1 10 11 12	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 >. <-> <. E , F >. Cgr <. B , C >. ) )
14	5 9 13	3anbi123d	\|- ( ( 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 >. ) <-> ( <. D , E >. Cgr <. A , B >. /\ <. D , F >. Cgr <. A , C >. /\ <. E , F >. Cgr <. B , C >. ) ) )
15		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 >. ) ) )
16		brcgr3	\|- ( ( N e. NN /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. D , <. E , F >. >. Cgr3 <. A , <. B , C >. >. <-> ( <. D , E >. Cgr <. A , B >. /\ <. D , F >. Cgr <. A , C >. /\ <. E , F >. Cgr <. B , C >. ) ) )
17	16	3com23	\|- ( ( 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 , F >. >. Cgr3 <. A , <. B , C >. >. <-> ( <. D , E >. Cgr <. A , B >. /\ <. D , F >. Cgr <. A , C >. /\ <. E , F >. Cgr <. B , C >. ) ) )
18	14 15 17	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 >. >. <-> <. D , <. E , F >. >. Cgr3 <. A , <. B , C >. >. ) )