df-colinear - Mathbox for Scott Fenton

	Mathbox for Scott Fenton		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-colinear		Structured version Visualization version Unicode version

Definition df-colinear 32146

Description: The colinearity predicate states that the three points in its arguments sit on one line. Definition 4.10 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 25-Oct-2013.)

**Assertion**
Ref	Expression
df-colinear	$/\$ $/\$ $/\$ $\/$ $\/$

Distinct variable group:

**Detailed syntax breakdown of Definition df-colinear**
Step	Hyp	Ref	Expression
1		ccolin 32144	. 2
2		va	. . . . . . . . 9
3	2	cv 1482	. . . . . . . 8
4		vn	. . . . . . . . . 10
5	4	cv 1482	. . . . . . . . 9
6		cee 25768	. . . . . . . . 9
7	5, 6	cfv 5888	. . . . . . . 8
8	3, 7	wcel 1990	. . . . . . 7
9		vb	. . . . . . . . 9
10	9	cv 1482	. . . . . . . 8
11	10, 7	wcel 1990	. . . . . . 7
12		vc	. . . . . . . . 9
13	12	cv 1482	. . . . . . . 8
14	13, 7	wcel 1990	. . . . . . 7
15	8, 11, 14	w3a 1037	. . . . . 6 $/\$ $/\$
16	10, 13	cop 4183	. . . . . . . 8
17		cbtwn 25769	. . . . . . . 8
18	3, 16, 17	wbr 4653	. . . . . . 7
19	13, 3	cop 4183	. . . . . . . 8
20	10, 19, 17	wbr 4653	. . . . . . 7
21	3, 10	cop 4183	. . . . . . . 8
22	13, 21, 17	wbr 4653	. . . . . . 7
23	18, 20, 22	w3o 1036	. . . . . 6 $\/$ $\/$
24	15, 23	wa 384	. . . . 5 $/\$ $/\$ $/\$ $\/$ $\/$
25		cn 11020	. . . . 5
26	24, 4, 25	wrex 2913	. . . 4 $/\$ $/\$ $/\$ $\/$ $\/$
27	26, 9, 12, 2	coprab 6651	. . 3 $/\$ $/\$ $/\$ $\/$ $\/$
28	27	ccnv 5113	. 2 $/\$ $/\$ $/\$ $\/$ $\/$
29	1, 28	wceq 1483	1 $/\$ $/\$ $/\$ $\/$ $\/$

Colors of variables: wff setvar class

This definition is referenced by: colinrel 32164 brcolinear2 32165 colinearex 32167 colineardim1 32168

W3C validator