Metamath Proof Explorer


Theorem tgcgrcoml

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 𝑃 = ( Base ‘ 𝐺 )
tkgeom.d = ( dist ‘ 𝐺 )
tkgeom.i 𝐼 = ( Itv ‘ 𝐺 )
tkgeom.g ( 𝜑𝐺 ∈ TarskiG )
tgcgrcomr.a ( 𝜑𝐴𝑃 )
tgcgrcomr.b ( 𝜑𝐵𝑃 )
tgcgrcomr.c ( 𝜑𝐶𝑃 )
tgcgrcomr.d ( 𝜑𝐷𝑃 )
tgcgrcomr.6 ( 𝜑 → ( 𝐴 𝐵 ) = ( 𝐶 𝐷 ) )
Assertion tgcgrcoml ( 𝜑 → ( 𝐵 𝐴 ) = ( 𝐶 𝐷 ) )

Proof

Step Hyp Ref Expression
1 tkgeom.p 𝑃 = ( Base ‘ 𝐺 )
2 tkgeom.d = ( dist ‘ 𝐺 )
3 tkgeom.i 𝐼 = ( Itv ‘ 𝐺 )
4 tkgeom.g ( 𝜑𝐺 ∈ TarskiG )
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 ( 𝜑 → ( 𝐵 𝐴 ) = ( 𝐶 𝐷 ) )