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

Proof

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