Description: Identity law for points on lines. Theorem 4.18 of Schwabhauser p. 38. (Contributed by Scott Fenton, 7-Oct-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | lineid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2l | |
|
2 | simp2r | |
|
3 | simp3l | |
|
4 | 1 2 3 | 3jca | |
5 | linecgr | |
|
6 | 4 5 | syld3an2 | |
7 | simp1 | |
|
8 | simp3r | |
|
9 | cgrid2 | |
|
10 | 7 3 3 8 9 | syl13anc | |
11 | 6 10 | syld | |