Metamath Proof Explorer

Theorem cgr3permute1

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

Ref Expression
Assertion cgr3permute1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → A B C Cgr3 D E F ↔ A C B Cgr3 D F E

Proof

Step Hyp Ref Expression
1 id ⊢ N ∈ ℕ → N ∈ ℕ
2 3simpc ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N
3 3simpc ⊢ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N
4 cgrcomlr ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → B C Cgr E F ↔ C B Cgr F E
5 1 2 3 4 syl3an ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → B C Cgr E F ↔ C B Cgr F E
6 5 3anbi3d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → A B Cgr D E ∧ A C Cgr D F ∧ B C Cgr E F ↔ A B Cgr D E ∧ A C Cgr D F ∧ C B Cgr F E
7 3ancoma ⊢ A B Cgr D E ∧ A C Cgr D F ∧ C B Cgr F E ↔ A C Cgr D F ∧ A B Cgr D E ∧ C B Cgr F E
8 6 7 bitrdi ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → A B Cgr D E ∧ A C Cgr D F ∧ B C Cgr E F ↔ A C Cgr D F ∧ A B Cgr D E ∧ C B Cgr F E
9 brcgr3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → A B C Cgr3 D E F ↔ A B Cgr D E ∧ A C Cgr D F ∧ B C Cgr E F
10 biid ⊢ N ∈ ℕ ↔ N ∈ ℕ
11 3ancomb ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ↔ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N
12 3ancomb ⊢ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ↔ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N
13 brcgr3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → A C B Cgr3 D F E ↔ A C Cgr D F ∧ A B Cgr D E ∧ C B Cgr F E
14 10 11 12 13 syl3anb ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → A C B Cgr3 D F E ↔ A C Cgr D F ∧ A B Cgr D E ∧ C B Cgr F E
15 8 9 14 3bitr4d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → A B C Cgr3 D E F ↔ A C B Cgr3 D F E