# Metamath Proof Explorer

## Theorem cgr3rflx

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

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

### Proof

Step Hyp Ref Expression
1 cgrrflx ${⊢}\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\to ⟨{A},{B}⟩\mathrm{Cgr}⟨{A},{B}⟩$
2 1 3adant3r3 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to ⟨{A},{B}⟩\mathrm{Cgr}⟨{A},{B}⟩$
3 cgrrflx ${⊢}\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\to ⟨{A},{C}⟩\mathrm{Cgr}⟨{A},{C}⟩$
4 3 3adant3r2 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to ⟨{A},{C}⟩\mathrm{Cgr}⟨{A},{C}⟩$
5 cgrrflx ${⊢}\left({N}\in ℕ\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\to ⟨{B},{C}⟩\mathrm{Cgr}⟨{B},{C}⟩$
6 5 3adant3r1 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to ⟨{B},{C}⟩\mathrm{Cgr}⟨{B},{C}⟩$
7 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({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},⟨{B},{C}⟩⟩\mathrm{Cgr3}⟨{A},⟨{B},{C}⟩⟩↔\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{A},{B}⟩\wedge ⟨{A},{C}⟩\mathrm{Cgr}⟨{A},{C}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{B},{C}⟩\right)\right)$
8 7 3anidm23 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},⟨{B},{C}⟩⟩\mathrm{Cgr3}⟨{A},⟨{B},{C}⟩⟩↔\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{A},{B}⟩\wedge ⟨{A},{C}⟩\mathrm{Cgr}⟨{A},{C}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{B},{C}⟩\right)\right)$
9 2 4 6 8 mpbir3and ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to ⟨{A},⟨{B},{C}⟩⟩\mathrm{Cgr3}⟨{A},⟨{B},{C}⟩⟩$