Metamath Proof Explorer


Theorem cgr3rotl

Description: Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 1-Aug-2020)

Ref Expression
Hypotheses tgcgrxfr.p P = Base G
tgcgrxfr.m - ˙ = dist G
tgcgrxfr.i I = Itv G
tgcgrxfr.r ˙ = 𝒢 G
tgcgrxfr.g φ G 𝒢 Tarski
tgbtwnxfr.a φ A P
tgbtwnxfr.b φ B P
tgbtwnxfr.c φ C P
tgbtwnxfr.d φ D P
tgbtwnxfr.e φ E P
tgbtwnxfr.f φ F P
tgbtwnxfr.2 φ ⟨“ ABC ”⟩ ˙ ⟨“ DEF ”⟩
Assertion cgr3rotl φ ⟨“ BCA ”⟩ ˙ ⟨“ EFD ”⟩

Proof

Step Hyp Ref Expression
1 tgcgrxfr.p P = Base G
2 tgcgrxfr.m - ˙ = dist G
3 tgcgrxfr.i I = Itv G
4 tgcgrxfr.r ˙ = 𝒢 G
5 tgcgrxfr.g φ G 𝒢 Tarski
6 tgbtwnxfr.a φ A P
7 tgbtwnxfr.b φ B P
8 tgbtwnxfr.c φ C P
9 tgbtwnxfr.d φ D P
10 tgbtwnxfr.e φ E P
11 tgbtwnxfr.f φ F P
12 tgbtwnxfr.2 φ ⟨“ ABC ”⟩ ˙ ⟨“ DEF ”⟩
13 1 2 3 4 5 6 7 8 9 10 11 12 cgr3swap12 φ ⟨“ BAC ”⟩ ˙ ⟨“ EDF ”⟩
14 1 2 3 4 5 7 6 8 10 9 11 13 cgr3swap23 φ ⟨“ BCA ”⟩ ˙ ⟨“ EFD ”⟩