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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	ncolne.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	ncolne.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	ncolne.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	ncolne.2	⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
Assertion	ncolne2	⊢ ( 𝜑 → 𝑋 ≠ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		ncolne.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		ncolne.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		ncolne.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8		ncolne.2	⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
9	1 3 2 4 6 7 5 8	ncolcom	⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) )
10	1 2 3 4 5 7 6 9	ncolne1	⊢ ( 𝜑 → 𝑋 ≠ 𝑍 )