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
|- ( ph -> N e. NN )
endofsegidand.2
|- ( ph -> A e. ( EE ` N ) )
endofsegidand.3
|- ( ph -> B e. ( EE ` N ) )
endofsegidand.4
|- ( ph -> C e. ( EE ` N ) )
endofsegidand.5
|- ( ( ph /\ ps ) -> C Btwn <. A , B >. )
endofsegidand.6
|- ( ( ph /\ ps ) -> <. A , B >. Cgr <. A , C >. )
Assertion endofsegidand
|- ( ( ph /\ ps ) -> B = C )

Proof

Step Hyp Ref Expression
1 endofsegidand.1
 |-  ( ph -> N e. NN )
2 endofsegidand.2
 |-  ( ph -> A e. ( EE ` N ) )
3 endofsegidand.3
 |-  ( ph -> B e. ( EE ` N ) )
4 endofsegidand.4
 |-  ( ph -> C e. ( EE ` N ) )
5 endofsegidand.5
 |-  ( ( ph /\ ps ) -> C Btwn <. A , B >. )
6 endofsegidand.6
 |-  ( ( ph /\ ps ) -> <. A , B >. Cgr <. A , C >. )
7 endofsegid
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( C Btwn <. A , B >. /\ <. A , B >. Cgr <. A , C >. ) -> B = C ) )
8 1 2 4 3 7 syl13anc
 |-  ( ph -> ( ( C Btwn <. A , B >. /\ <. A , B >. Cgr <. A , C >. ) -> B = C ) )
9 8 adantr
 |-  ( ( ph /\ ps ) -> ( ( C Btwn <. A , B >. /\ <. A , B >. Cgr <. A , C >. ) -> B = C ) )
10 5 6 9 mp2and
 |-  ( ( ph /\ ps ) -> B = C )