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 | |- .~ = ( cgrG ` G ) |
||
| tgcgrxfr.g | |- ( ph -> G e. TarskiG ) |
||
| tgbtwnxfr.a | |- ( ph -> A e. P ) |
||
| tgbtwnxfr.b | |- ( ph -> B e. P ) |
||
| tgbtwnxfr.c | |- ( ph -> C e. P ) |
||
| tgbtwnxfr.d | |- ( ph -> D e. P ) |
||
| tgbtwnxfr.e | |- ( ph -> E e. P ) |
||
| tgbtwnxfr.f | |- ( ph -> F e. P ) |
||
| tgbtwnxfr.2 | |- ( ph -> <" A B C "> .~ <" D E F "> ) |
||
| Assertion | cgr3simp2 | |- ( ph -> ( B .- C ) = ( E .- F ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tgcgrxfr.p | |- P = ( Base ` G ) |
|
| 2 | tgcgrxfr.m | |- .- = ( dist ` G ) |
|
| 3 | tgcgrxfr.i | |- I = ( Itv ` G ) |
|
| 4 | tgcgrxfr.r | |- .~ = ( cgrG ` G ) |
|
| 5 | tgcgrxfr.g | |- ( ph -> G e. TarskiG ) |
|
| 6 | tgbtwnxfr.a | |- ( ph -> A e. P ) |
|
| 7 | tgbtwnxfr.b | |- ( ph -> B e. P ) |
|
| 8 | tgbtwnxfr.c | |- ( ph -> C e. P ) |
|
| 9 | tgbtwnxfr.d | |- ( ph -> D e. P ) |
|
| 10 | tgbtwnxfr.e | |- ( ph -> E e. P ) |
|
| 11 | tgbtwnxfr.f | |- ( ph -> F e. P ) |
|
| 12 | tgbtwnxfr.2 | |- ( ph -> <" A B C "> .~ <" D E F "> ) |
|
| 13 | 1 2 4 5 6 7 8 9 10 11 | trgcgrg | |- ( ph -> ( <" A B C "> .~ <" D E F "> <-> ( ( A .- B ) = ( D .- E ) /\ ( B .- C ) = ( E .- F ) /\ ( C .- A ) = ( F .- D ) ) ) ) |
| 14 | 12 13 | mpbid | |- ( ph -> ( ( A .- B ) = ( D .- E ) /\ ( B .- C ) = ( E .- F ) /\ ( C .- A ) = ( F .- D ) ) ) |
| 15 | 14 | simp2d | |- ( ph -> ( B .- C ) = ( E .- F ) ) |