Metamath Proof Explorer

Theorem cgr3tr4

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

Ref Expression
Assertion cgr3tr4 ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝐸 , 𝐹 ⟩ ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝐻 , 𝐼 ⟩ ⟩ ) → ⟨ 𝐷 , ⟨ 𝐸 , 𝐹 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝐻 , 𝐼 ⟩ ⟩ ) )

Proof

Step Hyp Ref Expression
1 3an6 ⊢ ( ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐺 , 𝐼 ⟩ ) ∧ ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐻 , 𝐼 ⟩ ) ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐺 , 𝐼 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐻 , 𝐼 ⟩ ) ) )
2 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝑁 ∈ ℕ )
3 simpr11 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
4 simpr12 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
5 simpr21 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
6 simpr22 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
7 simpr31 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) )
8 simpr32 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) )
9 axcgrtr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) → ⟨ 𝐷 , 𝐸 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) )
10 2 3 4 5 6 7 8 9 syl133anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) → ⟨ 𝐷 , 𝐸 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) )
11 simpr13 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
12 simpr23 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) )
13 simpr33 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) )
14 axcgrtr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐺 , 𝐼 ⟩ ) → ⟨ 𝐷 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝐼 ⟩ ) )
15 2 3 11 5 12 7 13 14 syl133anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐺 , 𝐼 ⟩ ) → ⟨ 𝐷 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝐼 ⟩ ) )
16 axcgrtr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐻 , 𝐼 ⟩ ) → ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐻 , 𝐼 ⟩ ) )
17 2 4 11 6 12 8 13 16 syl133anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐻 , 𝐼 ⟩ ) → ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐻 , 𝐼 ⟩ ) )
18 10 15 17 3anim123d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐺 , 𝐼 ⟩ ) ∧ ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐻 , 𝐼 ⟩ ) ) → ( ⟨ 𝐷 , 𝐸 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐷 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝐼 ⟩ ∧ ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐻 , 𝐼 ⟩ ) ) )
19 1 18 syl5bir ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐺 , 𝐼 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐻 , 𝐼 ⟩ ) ) → ( ⟨ 𝐷 , 𝐸 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐷 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝐼 ⟩ ∧ ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐻 , 𝐼 ⟩ ) ) )
20 brcgr3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝐸 , 𝐹 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) )
21 20 3adant3r3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝐸 , 𝐹 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) )
22 brcgr3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝐻 , 𝐼 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐺 , 𝐼 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐻 , 𝐼 ⟩ ) ) )
23 22 3adant3r2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝐻 , 𝐼 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐺 , 𝐼 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐻 , 𝐼 ⟩ ) ) )
24 21 23 anbi12d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝐸 , 𝐹 ⟩ ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝐻 , 𝐼 ⟩ ⟩ ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐺 , 𝐼 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐻 , 𝐼 ⟩ ) ) ) )
25 brcgr3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐷 , ⟨ 𝐸 , 𝐹 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝐻 , 𝐼 ⟩ ⟩ ↔ ( ⟨ 𝐷 , 𝐸 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐷 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝐼 ⟩ ∧ ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐻 , 𝐼 ⟩ ) ) )
26 25 3adant3r1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ⟨ 𝐷 , ⟨ 𝐸 , 𝐹 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝐻 , 𝐼 ⟩ ⟩ ↔ ( ⟨ 𝐷 , 𝐸 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ∧ ⟨ 𝐷 , 𝐹 ⟩ Cgr ⟨ 𝐺 , 𝐼 ⟩ ∧ ⟨ 𝐸 , 𝐹 ⟩ Cgr ⟨ 𝐻 , 𝐼 ⟩ ) ) )
27 19 24 26 3imtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝐸 , 𝐹 ⟩ ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝐻 , 𝐼 ⟩ ⟩ ) → ⟨ 𝐷 , ⟨ 𝐸 , 𝐹 ⟩ ⟩ Cgr3 ⟨ 𝐺 , ⟨ 𝐻 , 𝐼 ⟩ ⟩ ) )