Metamath Proof Explorer

Theorem cgr3com

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

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

Proof

Step Hyp Ref Expression
1 id ⊢ N ∈ ℕ → N ∈ ℕ
2 3simpa ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N
3 3simpa ⊢ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N
4 cgrcom ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → A B Cgr D E ↔ D E Cgr A B
5 1 2 3 4 syl3an ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → A B Cgr D E ↔ D E Cgr A B
6 3simpb ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N
7 3simpb ⊢ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N
8 cgrcom ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → A C Cgr D F ↔ D F Cgr A C
9 1 6 7 8 syl3an ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → A C Cgr D F ↔ D F Cgr A C
10 3simpc ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N
11 3simpc ⊢ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N
12 cgrcom ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → B C Cgr E F ↔ E F Cgr B C
13 1 10 11 12 syl3an ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → B C Cgr E F ↔ E F Cgr B C
14 5 9 13 3anbi123d ⊢ 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 ↔ D E Cgr A B ∧ D F Cgr A C ∧ E F Cgr B C
15 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
16 brcgr3 ⊢ N ∈ ℕ ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → D E F Cgr3 A B C ↔ D E Cgr A B ∧ D F Cgr A C ∧ E F Cgr B C
17 16 3com23 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → D E F Cgr3 A B C ↔ D E Cgr A B ∧ D F Cgr A C ∧ E F Cgr B C
18 14 15 17 3bitr4d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → A B C Cgr3 D E F ↔ D E F Cgr3 A B C