Description: Permutation law for three-place congruence. (Contributed by Thierry Arnoux, 1-Aug-2020)
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 | cgr3rotl | ⊢ ( 𝜑 → 〈“ 𝐵 𝐶 𝐴 ”〉 ∼ 〈“ 𝐸 𝐹 𝐷 ”〉 ) |
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 | cgr3swap12 | ⊢ ( 𝜑 → 〈“ 𝐵 𝐴 𝐶 ”〉 ∼ 〈“ 𝐸 𝐷 𝐹 ”〉 ) |
14 | 1 2 3 4 5 7 6 8 10 9 11 13 | cgr3swap23 | ⊢ ( 𝜑 → 〈“ 𝐵 𝐶 𝐴 ”〉 ∼ 〈“ 𝐸 𝐹 𝐷 ”〉 ) |