Theorem tgbcne

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

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

Proof

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