Metamath Proof Explorer


Theorem endofsegidand

Description: Deduction form of endofsegid . (Contributed by Scott Fenton, 15-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses endofsegidand.1 ( 𝜑𝑁 ∈ ℕ )
endofsegidand.2 ( 𝜑𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
endofsegidand.3 ( 𝜑𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
endofsegidand.4 ( 𝜑𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
endofsegidand.5 ( ( 𝜑𝜓 ) → 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ )
endofsegidand.6 ( ( 𝜑𝜓 ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ )
Assertion endofsegidand ( ( 𝜑𝜓 ) → 𝐵 = 𝐶 )

Proof

Step Hyp Ref Expression
1 endofsegidand.1 ( 𝜑𝑁 ∈ ℕ )
2 endofsegidand.2 ( 𝜑𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
3 endofsegidand.3 ( 𝜑𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
4 endofsegidand.4 ( 𝜑𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
5 endofsegidand.5 ( ( 𝜑𝜓 ) → 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ )
6 endofsegidand.6 ( ( 𝜑𝜓 ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ )
7 endofsegid ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ ) → 𝐵 = 𝐶 ) )
8 1 2 4 3 7 syl13anc ( 𝜑 → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ ) → 𝐵 = 𝐶 ) )
9 8 adantr ( ( 𝜑𝜓 ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐴 , 𝐶 ⟩ ) → 𝐵 = 𝐶 ) )
10 5 6 9 mp2and ( ( 𝜑𝜓 ) → 𝐵 = 𝐶 )