Metamath Proof Explorer


Theorem cgr3permute3

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

Ref Expression
Assertion cgr3permute3 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B C Cgr3 D E F B C A Cgr3 E F D

Proof

Step Hyp Ref Expression
1 id N N
2 3simpa A 𝔼 N B 𝔼 N C 𝔼 N A 𝔼 N B 𝔼 N
3 3simpa D 𝔼 N E 𝔼 N F 𝔼 N D 𝔼 N E 𝔼 N
4 cgrcomlr N A 𝔼 N B 𝔼 N D 𝔼 N E 𝔼 N A B Cgr D E B A Cgr E D
5 1 2 3 4 syl3an N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B Cgr D E B A Cgr E D
6 3simpb A 𝔼 N B 𝔼 N C 𝔼 N A 𝔼 N C 𝔼 N
7 3simpb D 𝔼 N E 𝔼 N F 𝔼 N D 𝔼 N F 𝔼 N
8 cgrcomlr N A 𝔼 N C 𝔼 N D 𝔼 N F 𝔼 N A C Cgr D F C A Cgr F D
9 1 6 7 8 syl3an N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A C Cgr D F C A Cgr F D
10 5 9 3anbi12d N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B Cgr D E A C Cgr D F B C Cgr E F B A Cgr E D C A Cgr F D B C Cgr E F
11 3anrot B C Cgr E F B A Cgr E D C A Cgr F D B A Cgr E D C A Cgr F D B C Cgr E F
12 10 11 bitr4di N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B Cgr D E A C Cgr D F B C Cgr E F B C Cgr E F B A Cgr E D C A Cgr F D
13 brcgr3 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B C Cgr3 D E F A B Cgr D E A C Cgr D F B C Cgr E F
14 biid N N
15 3anrot A 𝔼 N B 𝔼 N C 𝔼 N B 𝔼 N C 𝔼 N A 𝔼 N
16 3anrot D 𝔼 N E 𝔼 N F 𝔼 N E 𝔼 N F 𝔼 N D 𝔼 N
17 brcgr3 N B 𝔼 N C 𝔼 N A 𝔼 N E 𝔼 N F 𝔼 N D 𝔼 N B C A Cgr3 E F D B C Cgr E F B A Cgr E D C A Cgr F D
18 14 15 16 17 syl3anb N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N B C A Cgr3 E F D B C Cgr E F B A Cgr E D C A Cgr F D
19 12 13 18 3bitr4d N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B C Cgr3 D E F B C A Cgr3 E F D