Metamath Proof Explorer

Theorem cgrsub

Description: Removing identical parts from the end of a line segment preserves congruence. Theorem 4.3 of Schwabhauser p. 35. (Contributed by Scott Fenton, 4-Oct-2013)

Ref Expression
Assertion cgrsub ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ) )

Proof

Step Hyp Ref Expression
1 simprl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) )
2 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ) → ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) )
3 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ) → 𝑁 ∈ ℕ )
4 simpl21 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
5 simpl31 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
6 cgrtriv ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ⟨ 𝐴 , 𝐴 ⟩ Cgr ⟨ 𝐷 , 𝐷 ⟩ )
7 3 4 5 6 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ) → ⟨ 𝐴 , 𝐴 ⟩ Cgr ⟨ 𝐷 , 𝐷 ⟩ )
8 simprrl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ) → ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ )
9 simpl23 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
10 simpl33 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ) → 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) )
11 cgrcomlr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ↔ ⟨ 𝐶 , 𝐴 ⟩ Cgr ⟨ 𝐹 , 𝐷 ⟩ ) )
12 3 4 9 5 10 11 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ) → ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ↔ ⟨ 𝐶 , 𝐴 ⟩ Cgr ⟨ 𝐹 , 𝐷 ⟩ ) )
13 8 12 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ) → ⟨ 𝐶 , 𝐴 ⟩ Cgr ⟨ 𝐹 , 𝐷 ⟩ )
14 7 13 jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ) → ( ⟨ 𝐴 , 𝐴 ⟩ Cgr ⟨ 𝐷 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐴 ⟩ Cgr ⟨ 𝐹 , 𝐷 ⟩ ) )
15 simpl22 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
16 simpl32 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
17 brifs ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐴 ⟩ ⟩ InnerFiveSeg ⟨ ⟨ 𝐷 , 𝐸 ⟩ , ⟨ 𝐹 , 𝐷 ⟩ ⟩ ↔ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐴 ⟩ Cgr ⟨ 𝐷 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐴 ⟩ Cgr ⟨ 𝐹 , 𝐷 ⟩ ) ) ) )
18 ifscgr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐴 ⟩ ⟩ InnerFiveSeg ⟨ ⟨ 𝐷 , 𝐸 ⟩ , ⟨ 𝐹 , 𝐷 ⟩ ⟩ → ⟨ 𝐵 , 𝐴 ⟩ Cgr ⟨ 𝐸 , 𝐷 ⟩ ) )
19 17 18 sylbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐴 ⟩ Cgr ⟨ 𝐷 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐴 ⟩ Cgr ⟨ 𝐹 , 𝐷 ⟩ ) ) → ⟨ 𝐵 , 𝐴 ⟩ Cgr ⟨ 𝐸 , 𝐷 ⟩ ) )
20 3 4 15 9 4 5 16 10 5 19 syl333anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ) → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐴 ⟩ Cgr ⟨ 𝐷 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐴 ⟩ Cgr ⟨ 𝐹 , 𝐷 ⟩ ) ) → ⟨ 𝐵 , 𝐴 ⟩ Cgr ⟨ 𝐸 , 𝐷 ⟩ ) )
21 1 2 14 20 mp3and ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ) → ⟨ 𝐵 , 𝐴 ⟩ Cgr ⟨ 𝐸 , 𝐷 ⟩ )
22 cgrcomlr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐵 , 𝐴 ⟩ Cgr ⟨ 𝐸 , 𝐷 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ) )
23 3 15 4 16 5 22 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ) → ( ⟨ 𝐵 , 𝐴 ⟩ Cgr ⟨ 𝐸 , 𝐷 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ) )
24 21 23 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ )
25 24 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐹 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ) )