Metamath Proof Explorer


Theorem cgr3permute5

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

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

Proof

Step Hyp Ref Expression
1 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
2 biid N N
3 3anrot A 𝔼 N B 𝔼 N C 𝔼 N B 𝔼 N C 𝔼 N A 𝔼 N
4 3anrot D 𝔼 N E 𝔼 N F 𝔼 N E 𝔼 N F 𝔼 N D 𝔼 N
5 cgr3permute2 N B 𝔼 N C 𝔼 N A 𝔼 N E 𝔼 N F 𝔼 N D 𝔼 N B C A Cgr3 E F D C B A Cgr3 F E D
6 2 3 4 5 syl3anb N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N B C A Cgr3 E F D C B A Cgr3 F E D
7 1 6 bitrd N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B C Cgr3 D E F C B A Cgr3 F E D