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 ⊢ φ → N ∈ ℕ
endofsegidand.2 ⊢ φ → A ∈ 𝔼 ⁡ N
endofsegidand.3 ⊢ φ → B ∈ 𝔼 ⁡ N
endofsegidand.4 ⊢ φ → C ∈ 𝔼 ⁡ N
endofsegidand.5 ⊢ φ ∧ ψ → C Btwn A B
endofsegidand.6 ⊢ φ ∧ ψ → A B Cgr A C
Assertion endofsegidand ⊢ φ ∧ ψ → B = C

Proof

Step Hyp Ref Expression
1 endofsegidand.1 ⊢ φ → N ∈ ℕ
2 endofsegidand.2 ⊢ φ → A ∈ 𝔼 ⁡ N
3 endofsegidand.3 ⊢ φ → B ∈ 𝔼 ⁡ N
4 endofsegidand.4 ⊢ φ → C ∈ 𝔼 ⁡ N
5 endofsegidand.5 ⊢ φ ∧ ψ → C Btwn A B
6 endofsegidand.6 ⊢ φ ∧ ψ → A B Cgr A C
7 endofsegid ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → C Btwn A B ∧ A B Cgr A C → B = C
8 1 2 4 3 7 syl13anc ⊢ φ → C Btwn A B ∧ A B Cgr A C → B = C
9 8 adantr ⊢ φ ∧ ψ → C Btwn A B ∧ A B Cgr A C → B = C
10 5 6 9 mp2and ⊢ φ ∧ ψ → B = C