Metamath Proof Explorer


Theorem cgr3permute4

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

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

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 cgr3permute3 N B 𝔼 N C 𝔼 N A 𝔼 N E 𝔼 N F 𝔼 N D 𝔼 N B C A Cgr3 E F D C A B Cgr3 F D E
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 A B Cgr3 F D E
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 A B Cgr3 F D E