Metamath Proof Explorer


Theorem trgcgr

Description: Triangle congruence. (Contributed by Thierry Arnoux, 27-Apr-2019)

Ref Expression
Hypotheses trgcgrg.p P=BaseG
trgcgrg.m -˙=distG
trgcgrg.r ˙=𝒢G
trgcgrg.g φG𝒢Tarski
trgcgrg.a φAP
trgcgrg.b φBP
trgcgrg.c φCP
trgcgrg.d φDP
trgcgrg.e φEP
trgcgrg.f φFP
trgcgr.1 φA-˙B=D-˙E
trgcgr.2 φB-˙C=E-˙F
trgcgr.3 φC-˙A=F-˙D
Assertion trgcgr φ⟨“ABC”⟩˙⟨“DEF”⟩

Proof

Step Hyp Ref Expression
1 trgcgrg.p P=BaseG
2 trgcgrg.m -˙=distG
3 trgcgrg.r ˙=𝒢G
4 trgcgrg.g φG𝒢Tarski
5 trgcgrg.a φAP
6 trgcgrg.b φBP
7 trgcgrg.c φCP
8 trgcgrg.d φDP
9 trgcgrg.e φEP
10 trgcgrg.f φFP
11 trgcgr.1 φA-˙B=D-˙E
12 trgcgr.2 φB-˙C=E-˙F
13 trgcgr.3 φC-˙A=F-˙D
14 1 2 3 4 5 6 7 8 9 10 trgcgrg φ⟨“ABC”⟩˙⟨“DEF”⟩A-˙B=D-˙EB-˙C=E-˙FC-˙A=F-˙D
15 11 12 13 14 mpbir3and φ⟨“ABC”⟩˙⟨“DEF”⟩