Theorem cgr3rflx

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

	Ref	Expression
Assertion	cgr3rflx	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ )

Proof

Step	Hyp	Ref	Expression
1		cgrrflx	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ )
2	1	3adant3r3	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ )
3		cgrrflx	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ )
4	3	3adant3r2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ )
5		cgrrflx	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ )
6	5	3adant3r1	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ )
7		brcgr3	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )
8	7	3anidm23	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )
9	2 4 6 8	mpbir3and	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ )