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	|- P = ( Base ` G )
	tgbcne.i	|- I = ( Itv ` G )
	tgbcne.l	|- L = ( LineG ` G )
	tgbcne.g	|- ( ph -> G e. TarskiG )
	tgbcne.a	|- ( ph -> A e. P )
	tgbcne.b	|- ( ph -> B e. P )
	tgbcne.c	|- ( ph -> C e. P )
	tgbcne.ncol	|- ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
Assertion	tgbcne	|- ( ph -> B =/= C )

Proof

Step	Hyp	Ref	Expression
1		tgbcne.p	|- P = ( Base ` G )
2		tgbcne.i	|- I = ( Itv ` G )
3		tgbcne.l	|- L = ( LineG ` G )
4		tgbcne.g	|- ( ph -> G e. TarskiG )
5		tgbcne.a	|- ( ph -> A e. P )
6		tgbcne.b	|- ( ph -> B e. P )
7		tgbcne.c	|- ( ph -> C e. P )
8		tgbcne.ncol	|- ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
9	1 3 2 4 5 6 7 8	ncolrot2	|- ( ph -> -. ( B e. ( C L A ) \/ C = A ) )
10	1 2 3 4 6 7 5 9	ncolne1	|- ( ph -> B =/= C )