Metamath Proof Explorer


Theorem cgr3permute1

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

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

Proof

Step Hyp Ref Expression
1 id N N
2 3simpc A 𝔼 N B 𝔼 N C 𝔼 N B 𝔼 N C 𝔼 N
3 3simpc D 𝔼 N E 𝔼 N F 𝔼 N E 𝔼 N F 𝔼 N
4 cgrcomlr N B 𝔼 N C 𝔼 N E 𝔼 N F 𝔼 N B C Cgr E F C B Cgr F E
5 1 2 3 4 syl3an N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N B C Cgr E F C B Cgr F E
6 5 3anbi3d 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 A B Cgr D E A C Cgr D F C B Cgr F E
7 3ancoma A B Cgr D E A C Cgr D F C B Cgr F E A C Cgr D F A B Cgr D E C B Cgr F E
8 6 7 bitrdi 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 A C Cgr D F A B Cgr D E C B Cgr F E
9 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
10 biid N N
11 3ancomb A 𝔼 N B 𝔼 N C 𝔼 N A 𝔼 N C 𝔼 N B 𝔼 N
12 3ancomb D 𝔼 N E 𝔼 N F 𝔼 N D 𝔼 N F 𝔼 N E 𝔼 N
13 brcgr3 N A 𝔼 N C 𝔼 N B 𝔼 N D 𝔼 N F 𝔼 N E 𝔼 N A C B Cgr3 D F E A C Cgr D F A B Cgr D E C B Cgr F E
14 10 11 12 13 syl3anb N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A C B Cgr3 D F E A C Cgr D F A B Cgr D E C B Cgr F E
15 8 9 14 3bitr4d N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B C Cgr3 D E F A C B Cgr3 D F E