Description: Congruence commutes on the LHS. Variant of Theorem 2.5 of Schwabhauser p. 27, but in a convenient form for a common case. (Contributed by David A. Wheeler, 29-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tkgeom.p | ||
tkgeom.d | |||
tkgeom.i | |||
tkgeom.g | |||
tgcgrcomr.a | |||
tgcgrcomr.b | |||
tgcgrcomr.c | |||
tgcgrcomr.d | |||
tgcgrcomr.6 | |||
Assertion | tgcgrcoml |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tkgeom.p | ||
2 | tkgeom.d | ||
3 | tkgeom.i | ||
4 | tkgeom.g | ||
5 | tgcgrcomr.a | ||
6 | tgcgrcomr.b | ||
7 | tgcgrcomr.c | ||
8 | tgcgrcomr.d | ||
9 | tgcgrcomr.6 | ||
10 | 1 2 3 4 5 6 | axtgcgrrflx | |
11 | 10 9 | eqtr3d |