Metamath Proof Explorer


Theorem tgcgrneq

Description: Congruence and equality. (Contributed by Thierry Arnoux, 27-Aug-2019)

Ref Expression
Hypotheses tkgeom.p 𝑃 = ( Base ‘ 𝐺 )
tkgeom.d = ( dist ‘ 𝐺 )
tkgeom.i 𝐼 = ( Itv ‘ 𝐺 )
tkgeom.g ( 𝜑𝐺 ∈ TarskiG )
tgcgrcomlr.a ( 𝜑𝐴𝑃 )
tgcgrcomlr.b ( 𝜑𝐵𝑃 )
tgcgrcomlr.c ( 𝜑𝐶𝑃 )
tgcgrcomlr.d ( 𝜑𝐷𝑃 )
tgcgrcomlr.6 ( 𝜑 → ( 𝐴 𝐵 ) = ( 𝐶 𝐷 ) )
tgcgrneq.1 ( 𝜑𝐴𝐵 )
Assertion tgcgrneq ( 𝜑𝐶𝐷 )

Proof

Step Hyp Ref Expression
1 tkgeom.p 𝑃 = ( Base ‘ 𝐺 )
2 tkgeom.d = ( dist ‘ 𝐺 )
3 tkgeom.i 𝐼 = ( Itv ‘ 𝐺 )
4 tkgeom.g ( 𝜑𝐺 ∈ TarskiG )
5 tgcgrcomlr.a ( 𝜑𝐴𝑃 )
6 tgcgrcomlr.b ( 𝜑𝐵𝑃 )
7 tgcgrcomlr.c ( 𝜑𝐶𝑃 )
8 tgcgrcomlr.d ( 𝜑𝐷𝑃 )
9 tgcgrcomlr.6 ( 𝜑 → ( 𝐴 𝐵 ) = ( 𝐶 𝐷 ) )
10 tgcgrneq.1 ( 𝜑𝐴𝐵 )
11 1 2 3 4 5 6 7 8 9 tgcgreqb ( 𝜑 → ( 𝐴 = 𝐵𝐶 = 𝐷 ) )
12 11 necon3bid ( 𝜑 → ( 𝐴𝐵𝐶𝐷 ) )
13 10 12 mpbid ( 𝜑𝐶𝐷 )