Description: The binary relation form of the colinearity predicate. (Contributed by Scott Fenton, 5-Oct-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | brcolinear | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brcolinear2 | |
|
2 | 1 | 3adant1 | |
3 | 2 | adantl | |
4 | simpr | |
|
5 | 4 | rexlimivw | |
6 | fveq2 | |
|
7 | 6 | eleq2d | |
8 | 6 | eleq2d | |
9 | 6 | eleq2d | |
10 | 7 8 9 | 3anbi123d | |
11 | 10 | anbi1d | |
12 | 11 | rspcev | |
13 | 12 | expr | |
14 | 5 13 | impbid2 | |
15 | 3 14 | bitrd | |