Metamath Proof Explorer


Theorem cgr3swap12

Description: Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 27-Apr-2019)

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 cgr3swap12 φ ⟨“ BAC ”⟩ ˙ ⟨“ EDF ”⟩

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 cgr3simp1 φ A - ˙ B = D - ˙ E
14 1 2 3 5 6 7 9 10 13 tgcgrcomlr φ B - ˙ A = E - ˙ D
15 1 2 3 4 5 6 7 8 9 10 11 12 cgr3simp3 φ C - ˙ A = F - ˙ D
16 1 2 3 5 8 6 11 9 15 tgcgrcomlr φ A - ˙ C = D - ˙ F
17 1 2 3 4 5 6 7 8 9 10 11 12 cgr3simp2 φ B - ˙ C = E - ˙ F
18 1 2 3 5 7 8 10 11 17 tgcgrcomlr φ C - ˙ B = F - ˙ E
19 1 2 4 5 7 6 8 10 9 11 14 16 18 trgcgr φ ⟨“ BAC ”⟩ ˙ ⟨“ EDF ”⟩