Metamath Proof Explorer


Theorem cgrtr3

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

Ref Expression
Assertion cgrtr3 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B Cgr E F C D Cgr E F A B Cgr C D

Proof

Step Hyp Ref Expression
1 simp1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N N
2 simp21 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A 𝔼 N
3 simp22 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N B 𝔼 N
4 simp32 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N E 𝔼 N
5 simp33 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N F 𝔼 N
6 simp23 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N C 𝔼 N
7 simp31 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N D 𝔼 N
8 simprl N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B Cgr E F C D Cgr E F A B Cgr E F
9 simprr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B Cgr E F C D Cgr E F C D Cgr E F
10 1 6 7 4 5 9 cgrcomand N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B Cgr E F C D Cgr E F E F Cgr C D
11 1 2 3 4 5 6 7 8 10 cgrtrand N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B Cgr E F C D Cgr E F A B Cgr C D
12 11 ex N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B Cgr E F C D Cgr E F A B Cgr C D