Theorem tgacne

Description: Non-collinearity of triangle A B C implies distinct vertices A and C . (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	tgacne.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tgacne.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tgacne.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tgacne.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tgacne.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	tgacne.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	tgacne.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	tgacne.ncol	⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
Assertion	tgacne	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		tgacne.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tgacne.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		tgacne.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		tgacne.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tgacne.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6		tgacne.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7		tgacne.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8		tgacne.ncol	⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
9	1 3 2 4 5 6 7 8	ncolrot1	⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
10	1 3 2 4 6 7 5 9	ncolcom	⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐵 ) ∨ 𝐶 = 𝐵 ) )
11	1 2 3 4 5 7 6 10	ncolne1	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )