Theorem cgr3permute5

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

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

Proof

Step	Hyp	Ref	Expression
1		cgr3permute3	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝐸 , 𝐹 ⟩ ⟩ ↔ ⟨ 𝐵 , ⟨ 𝐶 , 𝐴 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝐹 , 𝐷 ⟩ ⟩ ) )
2		biid	⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ℕ )
3		3anrot	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) )
4		3anrot	⊢ ( ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) )
5		cgr3permute2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐵 , ⟨ 𝐶 , 𝐴 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝐹 , 𝐷 ⟩ ⟩ ↔ ⟨ 𝐶 , ⟨ 𝐵 , 𝐴 ⟩ ⟩ Cgr3 ⟨ 𝐹 , ⟨ 𝐸 , 𝐷 ⟩ ⟩ ) )
6	2 3 4 5	syl3anb	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐵 , ⟨ 𝐶 , 𝐴 ⟩ ⟩ Cgr3 ⟨ 𝐸 , ⟨ 𝐹 , 𝐷 ⟩ ⟩ ↔ ⟨ 𝐶 , ⟨ 𝐵 , 𝐴 ⟩ ⟩ Cgr3 ⟨ 𝐹 , ⟨ 𝐸 , 𝐷 ⟩ ⟩ ) )
7	1 6	bitrd	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝐸 , 𝐹 ⟩ ⟩ ↔ ⟨ 𝐶 , ⟨ 𝐵 , 𝐴 ⟩ ⟩ Cgr3 ⟨ 𝐹 , ⟨ 𝐸 , 𝐷 ⟩ ⟩ ) )