Metamath Proof Explorer


Theorem cgr3simp2

Description: Deduce segment congruence from a triangle congruence. This is a portion of CPCTC, focusing on a specific segment. (Contributed by Thierry Arnoux, 27-Apr-2019)

Ref Expression
Hypotheses tgcgrxfr.p P = Base G
tgcgrxfr.m - ˙ = dist G
tgcgrxfr.i I = Itv G
tgcgrxfr.r ˙ = 𝒢 G
tgcgrxfr.g φ G 𝒢 Tarski
tgbtwnxfr.a φ A P
tgbtwnxfr.b φ B P
tgbtwnxfr.c φ C P
tgbtwnxfr.d φ D P
tgbtwnxfr.e φ E P
tgbtwnxfr.f φ F P
tgbtwnxfr.2 φ ⟨“ ABC ”⟩ ˙ ⟨“ DEF ”⟩
Assertion cgr3simp2 φ B - ˙ C = E - ˙ F

Proof

Step Hyp Ref Expression
1 tgcgrxfr.p P = Base G
2 tgcgrxfr.m - ˙ = dist G
3 tgcgrxfr.i I = Itv G
4 tgcgrxfr.r ˙ = 𝒢 G
5 tgcgrxfr.g φ G 𝒢 Tarski
6 tgbtwnxfr.a φ A P
7 tgbtwnxfr.b φ B P
8 tgbtwnxfr.c φ C P
9 tgbtwnxfr.d φ D P
10 tgbtwnxfr.e φ E P
11 tgbtwnxfr.f φ F P
12 tgbtwnxfr.2 φ ⟨“ ABC ”⟩ ˙ ⟨“ DEF ”⟩
13 1 2 4 5 6 7 8 9 10 11 trgcgrg φ ⟨“ ABC ”⟩ ˙ ⟨“ DEF ”⟩ A - ˙ B = D - ˙ E B - ˙ C = E - ˙ F C - ˙ A = F - ˙ D
14 12 13 mpbid φ A - ˙ B = D - ˙ E B - ˙ C = E - ˙ F C - ˙ A = F - ˙ D
15 14 simp2d φ B - ˙ C = E - ˙ F