Theorem tgsss3

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	tgsss3	⊢ ( 𝜑 → ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( 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 6 7 5 9 10 8 12 13 11 15 16 14	tgsss1	⊢ ( 𝜑 → ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ )