Theorem tgsss2

Description: Third congruence theorem: SSS. Theorem 11.51 of Schwabhauser p. 109. (Contributed by Thierry Arnoux, 1-Aug-2020)

	Ref	Expression
Hypotheses	tgsas.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tgsas.m	⊢ − = ( dist ‘ 𝐺 )
	tgsas.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tgsas.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tgsas.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	tgsas.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	tgsas.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	tgsas.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	tgsas.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
	tgsas.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
	tgsss.1	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
	tgsss.2	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
	tgsss.3	⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) )
	tgsss.4	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
	tgsss.5	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
	tgsss.6	⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
Assertion	tgsss2	⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐹 𝐷 𝐸 ”⟩ )

Proof

Step	Hyp	Ref	Expression
1		tgsas.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tgsas.m	⊢ − = ( dist ‘ 𝐺 )
3		tgsas.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		tgsas.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tgsas.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6		tgsas.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7		tgsas.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8		tgsas.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9		tgsas.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10		tgsas.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11		tgsss.1	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
12		tgsss.2	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
13		tgsss.3	⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) )
14		tgsss.4	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
15		tgsss.5	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
16		tgsss.6	⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
17	1 2 3 4 7 5 6 10 8 9 13 11 12 16 14 15	tgsss1	⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐹 𝐷 𝐸 ”⟩ )