Metamath Proof Explorer

Theorem cgr3swap23

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

Ref Expression
Hypotheses tgcgrxfr.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgcgrxfr.m ⊢ − = ( dist ‘ 𝐺 )
tgcgrxfr.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgcgrxfr.r ⊢ ∼ = ( cgrG ‘ 𝐺 )
tgcgrxfr.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgbtwnxfr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tgbtwnxfr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tgbtwnxfr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
tgbtwnxfr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgbtwnxfr.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
tgbtwnxfr.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
tgbtwnxfr.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
Assertion cgr3swap23 ( 𝜑 → ⟨“ 𝐴 𝐶 𝐵 ”⟩ ∼ ⟨“ 𝐷 𝐹 𝐸 ”⟩ )

Proof

Step Hyp Ref Expression
1 tgcgrxfr.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgcgrxfr.m ⊢ − = ( dist ‘ 𝐺 )
3 tgcgrxfr.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tgcgrxfr.r ⊢ ∼ = ( cgrG ‘ 𝐺 )
5 tgcgrxfr.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 tgbtwnxfr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 tgbtwnxfr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 tgbtwnxfr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9 tgbtwnxfr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
10 tgbtwnxfr.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
11 tgbtwnxfr.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
12 tgbtwnxfr.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
13 1 2 3 4 5 6 7 8 9 10 11 12 cgr3simp3 ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) )
14 1 2 3 5 8 6 11 9 13 tgcgrcomlr ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )
15 1 2 3 4 5 6 7 8 9 10 11 12 cgr3simp2 ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
16 1 2 3 5 7 8 10 11 15 tgcgrcomlr ⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) = ( 𝐹 − 𝐸 ) )
17 1 2 3 4 5 6 7 8 9 10 11 12 cgr3simp1 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
18 1 2 3 5 6 7 9 10 17 tgcgrcomlr ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( 𝐸 − 𝐷 ) )
19 1 2 4 5 6 8 7 9 11 10 14 16 18 trgcgr ⊢ ( 𝜑 → ⟨“ 𝐴 𝐶 𝐵 ”⟩ ∼ ⟨“ 𝐷 𝐹 𝐸 ”⟩ )