Metamath Proof Explorer

Theorem btwntriv1

Description: Betweenness always holds for the first endpoint. Theorem 3.3 of Schwabhauser p. 30. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion btwntriv1 
|- ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> A Btwn <. A , B >. )

Proof

Step Hyp Ref Expression
1 btwntriv2 
 |-  ( ( N e. NN /\ B e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> A Btwn <. B , A >. )
2 1 3com23 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> A Btwn <. B , A >. )
3 simp1 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> N e. NN )
4 simp2 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> A e. ( EE ` N ) )
5 simp3 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> B e. ( EE ` N ) )
6 btwncom 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( A Btwn <. A , B >. <-> A Btwn <. B , A >. ) )
7 3 4 4 5 6 syl13anc 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A Btwn <. A , B >. <-> A Btwn <. B , A >. ) )
8 2 7 mpbird 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> A Btwn <. A , B >. )