Metamath Proof Explorer

Theorem cgr3rflx

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

Ref Expression
Assertion cgr3rflx ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A B C Cgr3 A B C

Proof

Step Hyp Ref Expression
1 cgrrflx ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A B Cgr A B
2 1 3adant3r3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A B Cgr A B
3 cgrrflx ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A C Cgr A C
4 3 3adant3r2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A C Cgr A C
5 cgrrflx ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → B C Cgr B C
6 5 3adant3r1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → B C Cgr B C
7 brcgr3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A B C Cgr3 A B C ↔ A B Cgr A B ∧ A C Cgr A C ∧ B C Cgr B C
8 7 3anidm23 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A B C Cgr3 A B C ↔ A B Cgr A B ∧ A C Cgr A C ∧ B C Cgr B C
9 2 4 6 8 mpbir3and ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A B C Cgr3 A B C