Metamath Proof Explorer


Theorem ncolne2

Description: Non-colinear points are different. (Contributed by Thierry Arnoux, 8-Aug-2019) TODO (NM): maybe ncolne2 could be simplified out and deleted, replaced by ncolcom .

Ref Expression
Hypotheses tglineelsb2.p B=BaseG
tglineelsb2.i I=ItvG
tglineelsb2.l L=Line𝒢G
tglineelsb2.g φG𝒢Tarski
ncolne.x φXB
ncolne.y φYB
ncolne.z φZB
ncolne.2 φ¬XYLZY=Z
Assertion ncolne2 φXZ

Proof

Step Hyp Ref Expression
1 tglineelsb2.p B=BaseG
2 tglineelsb2.i I=ItvG
3 tglineelsb2.l L=Line𝒢G
4 tglineelsb2.g φG𝒢Tarski
5 ncolne.x φXB
6 ncolne.y φYB
7 ncolne.z φZB
8 ncolne.2 φ¬XYLZY=Z
9 1 3 2 4 6 7 5 8 ncolcom φ¬XZLYZ=Y
10 1 2 3 4 5 7 6 9 ncolne1 φXZ