Theorem cgr3permute1

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

	Ref	Expression
Assertion	cgr3permute1	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝐸 , 𝐹 ⟩ ⟩ ↔ ⟨ 𝐴 , ⟨ 𝐶 , 𝐵 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝐹 , 𝐸 ⟩ ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ )
2		3simpc	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) )
3		3simpc	⊢ ( ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) )
4		cgrcomlr	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ↔ ⟨ 𝐶 , 𝐵 ⟩ Cgr ⟨ 𝐹 , 𝐸 ⟩ ) )
5	1 2 3 4	syl3an	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ↔ ⟨ 𝐶 , 𝐵 ⟩ Cgr ⟨ 𝐹 , 𝐸 ⟩ ) )
6	5	3anbi3d	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐵 ⟩ Cgr ⟨ 𝐹 , 𝐸 ⟩ ) ) )
7		3ancoma	⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐶 , 𝐵 ⟩ Cgr ⟨ 𝐹 , 𝐸 ⟩ ) ↔ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐶 , 𝐵 ⟩ Cgr ⟨ 𝐹 , 𝐸 ⟩ ) )
8	6 7	bitrdi	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ↔ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐶 , 𝐵 ⟩ Cgr ⟨ 𝐹 , 𝐸 ⟩ ) ) )
9		brcgr3	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝐸 , 𝐹 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) )
10		biid	⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ℕ )
11		3ancomb	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) )
12		3ancomb	⊢ ( ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) )
13		brcgr3	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , ⟨ 𝐶 , 𝐵 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝐹 , 𝐸 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐶 , 𝐵 ⟩ Cgr ⟨ 𝐹 , 𝐸 ⟩ ) ) )
14	10 11 12 13	syl3anb	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , ⟨ 𝐶 , 𝐵 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝐹 , 𝐸 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐶 , 𝐵 ⟩ Cgr ⟨ 𝐹 , 𝐸 ⟩ ) ) )
15	8 9 14	3bitr4d	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝐸 , 𝐹 ⟩ ⟩ ↔ ⟨ 𝐴 , ⟨ 𝐶 , 𝐵 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝐹 , 𝐸 ⟩ ⟩ ) )