# Metamath Proof Explorer

## Theorem cgr3permute3

Description: Permutation law for three-place congruence. (Contributed by Scott Fenton, 5-Oct-2013)

Ref Expression
Assertion cgr3permute3 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},⟨{B},{C}⟩⟩\mathrm{Cgr3}⟨{D},⟨{E},{F}⟩⟩↔⟨{B},⟨{C},{A}⟩⟩\mathrm{Cgr3}⟨{E},⟨{F},{D}⟩⟩\right)$

### Proof

Step Hyp Ref Expression
1 id ${⊢}{N}\in ℕ\to {N}\in ℕ$
2 3simpa ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\to \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)$
3 3simpa ${⊢}\left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\to \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)$
4 cgrcomlr ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩↔⟨{B},{A}⟩\mathrm{Cgr}⟨{E},{D}⟩\right)$
5 1 2 3 4 syl3an ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩↔⟨{B},{A}⟩\mathrm{Cgr}⟨{E},{D}⟩\right)$
6 3simpb ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\to \left({A}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)$
7 3simpb ${⊢}\left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\to \left({D}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)$
8 cgrcomlr ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩↔⟨{C},{A}⟩\mathrm{Cgr}⟨{F},{D}⟩\right)$
9 1 6 7 8 syl3an ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩↔⟨{C},{A}⟩\mathrm{Cgr}⟨{F},{D}⟩\right)$
10 5 9 3anbi12d ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\to \left(\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)↔\left(⟨{B},{A}⟩\mathrm{Cgr}⟨{E},{D}⟩\wedge ⟨{C},{A}⟩\mathrm{Cgr}⟨{F},{D}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)$
11 3anrot ${⊢}\left(⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\wedge ⟨{B},{A}⟩\mathrm{Cgr}⟨{E},{D}⟩\wedge ⟨{C},{A}⟩\mathrm{Cgr}⟨{F},{D}⟩\right)↔\left(⟨{B},{A}⟩\mathrm{Cgr}⟨{E},{D}⟩\wedge ⟨{C},{A}⟩\mathrm{Cgr}⟨{F},{D}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)$
12 10 11 syl6bbr ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\to \left(\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)↔\left(⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\wedge ⟨{B},{A}⟩\mathrm{Cgr}⟨{E},{D}⟩\wedge ⟨{C},{A}⟩\mathrm{Cgr}⟨{F},{D}⟩\right)\right)$
13 brcgr3 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},⟨{B},{C}⟩⟩\mathrm{Cgr3}⟨{D},⟨{E},{F}⟩⟩↔\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)$
14 biid ${⊢}{N}\in ℕ↔{N}\in ℕ$
15 3anrot ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)↔\left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)$
16 3anrot ${⊢}\left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)↔\left({E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)$
17 brcgr3 ${⊢}\left({N}\in ℕ\wedge \left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\wedge \left({E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{B},⟨{C},{A}⟩⟩\mathrm{Cgr3}⟨{E},⟨{F},{D}⟩⟩↔\left(⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\wedge ⟨{B},{A}⟩\mathrm{Cgr}⟨{E},{D}⟩\wedge ⟨{C},{A}⟩\mathrm{Cgr}⟨{F},{D}⟩\right)\right)$
18 14 15 16 17 syl3anb ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{B},⟨{C},{A}⟩⟩\mathrm{Cgr3}⟨{E},⟨{F},{D}⟩⟩↔\left(⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\wedge ⟨{B},{A}⟩\mathrm{Cgr}⟨{E},{D}⟩\wedge ⟨{C},{A}⟩\mathrm{Cgr}⟨{F},{D}⟩\right)\right)$
19 12 13 18 3bitr4d ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},⟨{B},{C}⟩⟩\mathrm{Cgr3}⟨{D},⟨{E},{F}⟩⟩↔⟨{B},⟨{C},{A}⟩⟩\mathrm{Cgr3}⟨{E},⟨{F},{D}⟩⟩\right)$