Metamath Proof Explorer

Theorem cgr3tr4

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

Ref Expression
Assertion cgr3tr4 
|- ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> ( ( <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. /\ <. A , <. B , C >. >. Cgr3 <. G , <. H , I >. >. ) -> <. D , <. E , F >. >. Cgr3 <. G , <. H , I >. >. ) )

Proof

Step Hyp Ref Expression
1 3an6 
 |-  ( ( ( <. A , B >. Cgr <. D , E >. /\ <. A , B >. Cgr <. G , H >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. A , C >. Cgr <. G , I >. ) /\ ( <. B , C >. Cgr <. E , F >. /\ <. B , C >. Cgr <. H , I >. ) ) <-> ( ( <. A , B >. Cgr <. D , E >. /\ <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) /\ ( <. A , B >. Cgr <. G , H >. /\ <. A , C >. Cgr <. G , I >. /\ <. B , C >. Cgr <. H , I >. ) ) )
2 simpl 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> N e. NN )
3 simpr11 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> A e. ( EE ` N ) )
4 simpr12 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> B e. ( EE ` N ) )
5 simpr21 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> D e. ( EE ` N ) )
6 simpr22 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> E e. ( EE ` N ) )
7 simpr31 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> G e. ( EE ` N ) )
8 simpr32 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> H e. ( EE ` N ) )
9 axcgrtr 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. A , B >. Cgr <. D , E >. /\ <. A , B >. Cgr <. G , H >. ) -> <. D , E >. Cgr <. G , H >. ) )
10 2 3 4 5 6 7 8 9 syl133anc 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> ( ( <. A , B >. Cgr <. D , E >. /\ <. A , B >. Cgr <. G , H >. ) -> <. D , E >. Cgr <. G , H >. ) )
11 simpr13 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> C e. ( EE ` N ) )
12 simpr23 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> F e. ( EE ` N ) )
13 simpr33 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> I e. ( EE ` N ) )
14 axcgrtr 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) -> ( ( <. A , C >. Cgr <. D , F >. /\ <. A , C >. Cgr <. G , I >. ) -> <. D , F >. Cgr <. G , I >. ) )
15 2 3 11 5 12 7 13 14 syl133anc 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> ( ( <. A , C >. Cgr <. D , F >. /\ <. A , C >. Cgr <. G , I >. ) -> <. D , F >. Cgr <. G , I >. ) )
16 axcgrtr 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) -> ( ( <. B , C >. Cgr <. E , F >. /\ <. B , C >. Cgr <. H , I >. ) -> <. E , F >. Cgr <. H , I >. ) )
17 2 4 11 6 12 8 13 16 syl133anc 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> ( ( <. B , C >. Cgr <. E , F >. /\ <. B , C >. Cgr <. H , I >. ) -> <. E , F >. Cgr <. H , I >. ) )
18 10 15 17 3anim123d 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> ( ( ( <. A , B >. Cgr <. D , E >. /\ <. A , B >. Cgr <. G , H >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. A , C >. Cgr <. G , I >. ) /\ ( <. B , C >. Cgr <. E , F >. /\ <. B , C >. Cgr <. H , I >. ) ) -> ( <. D , E >. Cgr <. G , H >. /\ <. D , F >. Cgr <. G , I >. /\ <. E , F >. Cgr <. H , I >. ) ) )
19 1 18 syl5bir 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> ( ( ( <. A , B >. Cgr <. D , E >. /\ <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) /\ ( <. A , B >. Cgr <. G , H >. /\ <. A , C >. Cgr <. G , I >. /\ <. B , C >. Cgr <. H , I >. ) ) -> ( <. D , E >. Cgr <. G , H >. /\ <. D , F >. Cgr <. G , I >. /\ <. E , F >. Cgr <. H , I >. ) ) )
20 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 >. ) ) )
21 20 3adant3r3 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I 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 >. ) ) )
22 brcgr3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) -> ( <. A , <. B , C >. >. Cgr3 <. G , <. H , I >. >. <-> ( <. A , B >. Cgr <. G , H >. /\ <. A , C >. Cgr <. G , I >. /\ <. B , C >. Cgr <. H , I >. ) ) )
23 22 3adant3r2 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> ( <. A , <. B , C >. >. Cgr3 <. G , <. H , I >. >. <-> ( <. A , B >. Cgr <. G , H >. /\ <. A , C >. Cgr <. G , I >. /\ <. B , C >. Cgr <. H , I >. ) ) )
24 21 23 anbi12d 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> ( ( <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. /\ <. A , <. B , C >. >. Cgr3 <. G , <. H , I >. >. ) <-> ( ( <. A , B >. Cgr <. D , E >. /\ <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) /\ ( <. A , B >. Cgr <. G , H >. /\ <. A , C >. Cgr <. G , I >. /\ <. B , C >. Cgr <. H , I >. ) ) ) )
25 brcgr3 
 |-  ( ( N e. NN /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) -> ( <. D , <. E , F >. >. Cgr3 <. G , <. H , I >. >. <-> ( <. D , E >. Cgr <. G , H >. /\ <. D , F >. Cgr <. G , I >. /\ <. E , F >. Cgr <. H , I >. ) ) )
26 25 3adant3r1 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> ( <. D , <. E , F >. >. Cgr3 <. G , <. H , I >. >. <-> ( <. D , E >. Cgr <. G , H >. /\ <. D , F >. Cgr <. G , I >. /\ <. E , F >. Cgr <. H , I >. ) ) )
27 19 24 26 3imtr4d 
 |-  ( ( 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 ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ I e. ( EE ` N ) ) ) ) -> ( ( <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. /\ <. A , <. B , C >. >. Cgr3 <. G , <. H , I >. >. ) -> <. D , <. E , F >. >. Cgr3 <. G , <. H , I >. >. ) )