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