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→ABCCgr3ABC

Proof

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