endofsegidand

Step	Hyp	Ref	Expression
1		endofsegidand.1	$⊢ φ \to N \in ℕ$
2		endofsegidand.2	$⊢ φ \to A \in 𝔼 (N)$
3		endofsegidand.3	$⊢ φ \to B \in 𝔼 (N)$
4		endofsegidand.4	$⊢ φ \to C \in 𝔼 (N)$
5		endofsegidand.5	$⊢ (φ \land ψ) \to C Btwn ⟨A, B⟩$
6		endofsegidand.6	$⊢ (φ \land ψ) \to ⟨A, B⟩ Cgr ⟨A, C⟩$
7		endofsegid	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N) \land B \in 𝔼 (N))) \to ((C Btwn ⟨A, B⟩ \land ⟨A, B⟩ Cgr ⟨A, C⟩) \to B = C)$
8	1 2 4 3 7	syl13anc	$⊢ φ \to ((C Btwn ⟨A, B⟩ \land ⟨A, B⟩ Cgr ⟨A, C⟩) \to B = C)$
9	8	adantr	$⊢ (φ \land ψ) \to ((C Btwn ⟨A, B⟩ \land ⟨A, B⟩ Cgr ⟨A, C⟩) \to B = C)$
10	5 6 9	mp2and	$⊢ (φ \land ψ) \to B = C$

Metamath Proof Explorer